1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import topology.local_homeomorph
src         └───────────────────────┘
  8  
  9  /-!
 10  # Manifolds
 11  
 12  A manifold is a topological space M locally modelled on a model space H, i.e., the manifold is
 13  covered by open subsets on which there are local homeomorphisms (the charts) going to H. If the
 14  changes of charts satisfy some additional property (for instance if they are smooth), then M
 15  inherits additional structure (it makes sense to talk about smooth manifolds). There are therefore
 16  two different ingredients in a manifold:
 17  * the set of charts, which is data
 18  * the fact that changes of charts belong to some group (in fact groupoid), which is additional Prop.
 19  
 20  We separate these two parts in the definition: the manifold structure is just the set of charts, and
 21  then the different smoothness requirements (smooth manifold, orientable manifold, contact manifold,
 22  and so on) are additional properties of these charts. These properties are formalized through the
 23  notion of structure groupoid, i.e., a set of local homeomorphisms stable under composition and
 24  inverse, to which the change of coordinates should belong.
 25  
 26  ## Main definitions
 27  * `structure_groupoid H`   : a subset of local homeomorphisms of `H` stable under composition, inverse
 28                               and restriction (ex: local diffeos)
 29  * `pregroupoid H`          : a subset of local homeomorphisms of `H` stable under composition and
 30                               restriction, but not inverse (ex: smooth maps)
 31  * `groupoid_of_pregroupoid`: construct a groupoid from a pregroupoid, by requiring that a map and its
 32                               inverse both belong to the pregroupoid (ex: construct diffeos from smooth
 33                               maps)
 34  * `continuous_groupoid H`  : the groupoid of all local homeomorphisms of `H`
 35  
 36  * `manifold H M`           : manifold structure on `M` modelled on `H`, given by an atlas of local
 37                               homeomorphisms from `M` to `H` whose sources cover `M`. This is a type class.
 38  * `has_groupoid M G`       : when `G` is a structure groupoid on `H` and `M` is a manifold modelled on
 39                               `H`, require that all coordinate changes belong to `G`. This is a type
 40                               class
 41  * `atlas H M`              : when `M` is a manifold modelled on `H`, the atlas of this manifold
 42                               structure, i.e., the set of charts
 43  * `structomorph G M M'`    : the set of diffeomorphisms between the manifolds `M` and `M'` for the
 44                               groupoid `G`. We avoid the word diffeomorphisms, keeping it for the
 45                               smooth category.
 46  
 47  As a basic example, we give the instance
 48  `instance manifold_model_space (H : Type*) [topological_space H] : manifold H H`
 49  saying that a topological space is a manifold over itself, with the identity as unique chart. This
 50  manifold structure is compatible with any groupoid.
 51  
 52  ## Implementation notes
 53  
 54  The atlas in a manifold is *not* a maximal atlas in general: the notion of maximality depends on the
 55  groupoid one considers, and changing groupoids changes the maximal atlas. With the current
 56  formalization, it makes sense first to choose the atlas, and then to ask whether this precise atlas
 57  defines a smooth manifold, an orientable manifold, and so on. A consequence is that structomorphisms
 58  between M and M' do *not* induce a bijection between the atlases of M and M': the definition is only
 59  that, read in charts, the structomorphism locally belongs to the groupoid under consideration.
 60  (This is equivalent to inducing a bijection between elements of the maximal atlas). A consequence
 61  is that the invariance under structomorphisms of properties defined in terms of the atlas is not
 62  obvious in general, and could require some work in theory (amounting to the fact that these
 63  properties only depend on the maximal atlas, for instance). In practice, this does not create any
 64  real difficulty.
 65  
 66  We use the letter `H` for the model space thinking of the case of manifolds with boundary, where the
 67  model space is a half space.
 68  
 69  Manifolds are sometimes defined as topological spaces with an atlas of local diffeomorphisms, and
 70  sometimes as spaces with an atlas from which a topology is deduced. We use the former approach:
 71  otherwise, there would be an instance from manifolds to topological spaces, which means that any
 72  instance search for topological spaces would try to find manifold structures involving a yet
 73  unknown model space, leading to problems. However, we also introduce the latter approach,
 74  through a structure `manifold_core` making it possible to construct a topology out of a set of local
 75  equivs with compatibility conditions (but we do not register it as an instance).
 76  
 77  In the definition of a manifold, the model space is written as an explicit parameter as there can be
 78  several model spaces for a given topological space. For instance, a complex manifold (modelled over
 79  ℂ^n) will also be seen sometimes as a real manifold modelled over ℝ^(2n).
 80  -/
 81  
 82  noncomputable theory
 83  local attribute [instance, priority 0] classical.decidable_inhabited classical.prop_decidable
id                                          └───────────────────────────┘ └──────────────────────┘
src                                         └───────────────────────────┘ └──────────────────────┘
typ                                         └───────────────────────────┘ └──────────────────────┘
 84  
 85  universes u
 86  
 87  variables {H : Type u} {M : Type*} {M' : Type*} {M'' : Type*}
 88  
 89  /- Notational shortcut for the composition of local homeomorphisms, i.e., `local_homeomorph.trans`.
 90  Note that, as is usual for equivs, the composition is from left to right, hence the direction of
 91  the arrow. -/
 92  local infixr  ` ≫ₕ `:100 := local_homeomorph.trans
id                               └────────────────────┘
src                              └────────────────────┘
typ                              └────────────────────┘
doc                              └────────────────────┘
 93  
 94  open set local_homeomorph
 95  
 96  section groupoid
 97  
 98  /- One could add to the definition of a structure groupoid the fact that the restriction of an
 99  element of the groupoid to any open set still belongs to the groupoid.
100  (This is in Kobayashi-Nomizu.)
101  I am not sure I want this, for instance on H × E where E is a vector space, and the groupoid is made
102  of functions respecting the fibers and linear in the fibers (so that a manifold over this groupoid
103  is naturally a vector bundle) I prefer that the members of the groupoid are always defined on
104  sets of the form s × E
105  
106  The only nontrivial requirement is locality: if a local homeomorphism belongs to the groupoid
107  around each point in its domain of definition, then it belongs to the groupoid. Without this
108  requirement, the composition of diffeomorphisms does not have to be a diffeomorphism. Note that
109  this implies that a local homeomorphism with empty source belongs to any structure groupoid, as
110  it trivially satisfies this condition.
111  
112  There is also a technical point, related to the fact that a local homeomorphism is by definition a
113  global map which is a homeomorphism when restricted to its source subset (and its values outside
114  of the source are not relevant). Therefore, we also require that being a member of the groupoid only
115  depends on the values on the source.
116  -/
117  /-- A structure groupoid is a set of local homeomorphisms of a topological space stable under
118  composition and inverse. They appear in the definition of the smoothness class of a manifold. -/
119  structure structure_groupoid (H : Type u) [topological_space H] :=
id                                     └──┘     └───────────────┘ 
src                                             └───────────────┘
typ                                    └──┘     └───────────────┘ 
doc                                             └───────────────┘
120  (members      : set (local_homeomorph H H))
id                   └─┘  └──────────────┘  
src                  └─┘  └──────────────┘
typ                  └─┘  └──────────────┘  
doc                       └──────────────┘
121  (comp         : ∀e e' : local_homeomorph H H, e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
id                          └──────────────┘      └─────┘   └┘  └─────┘    └┘ └┘  └─────┘
src                          └──────────────┘                                   └┘    
typ                         └──────────────┘      └─────┘   └┘  └─────┘    └┘ └┘  └─────┘
doc                          └──────────────┘                                     └┘
122  (inv          : ∀e : local_homeomorph H H, e ∈ members → e.symm ∈ members)
id                       └──────────────┘      └─────┘   └───┘  └─────┘
src                       └──────────────┘                    └───┘ 
typ                      └──────────────┘      └─────┘   └───┘  └─────┘
doc                       └──────────────┘                     └───┘
123  (id_mem       : local_homeomorph.refl H ∈ members)
id                   └───────────────────┘   └─────┘
src                  └───────────────────┘   
typ                  └───────────────────┘   └─────┘
doc                  └───────────────────┘
124  (locality     : ∀e : local_homeomorph H H, (∀x ∈ e.source, ∃s, is_open s ∧
id                       └──────────────┘         └─────┘   └─────┘  
src                       └──────────────┘            └─────┘    └─────┘   
typ                      └──────────────┘         └─────┘   └─────┘  
doc                       └──────────────┘                          └─────┘
125                    x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
id                         └────┘   └─────┘      └─────┘
src                           └────┘                 
typ                        └────┘   └─────┘      └─────┘
doc                             └────┘
126  (eq_on_source : ∀ e e' : local_homeomorph H H, e ∈ members → e' ≈ e → e' ∈ members)
id                           └──────────────┘      └─────┘   └┘     └┘  └─────┘
src                           └──────────────┘                              
typ                          └──────────────┘      └─────┘   └┘     └┘  └─────┘
doc                           └──────────────┘
127  
128  variable [topological_space H]
id             └───────────────┘
src            └───────────────┘
typ            └───────────────┘
doc            └───────────────┘
129  
130  @[reducible] instance : has_mem (local_homeomorph H H) (structure_groupoid H) :=
id                           └─────┘  └──────────────┘     └────────────────┘ 
src                          └─────┘  └──────────────┘       └────────────────┘
typ                          └─────┘  └──────────────┘     └────────────────┘ 
doc    └───────┘                      └──────────────┘       └────────────────┘
131  ⟨λ(e : local_homeomorph H H) (G : structure_groupoid H), e ∈ G.members⟩
id          └──────────────┘         └────────────────┘      └──────┘
src         └──────────────┘           └────────────────┘         └──────┘
typ         └──────────────┘         └────────────────┘      └──────┘
doc         └──────────────┘           └────────────────┘
132  
133  /-- Partial order on the set of groupoids, given by inclusion of the members of the groupoid -/
134  instance structure_groupoid.partial_order : partial_order (structure_groupoid H) :=
id                                               └───────────┘  └────────────────┘ 
src                                              └───────────┘  └────────────────┘
typ                                              └───────────┘  └────────────────┘ 
doc                                                             └────────────────┘
135  partial_order.lift structure_groupoid.members
id   └────────────────┘ └────────────────────────┘
src  └────────────────┘ └────────────────────────┘
typ  └────────────────┘ └────────────────────────┘
136  (λa b h, by { cases a, cases b, dsimp at h, induction h, refl }) (by apply_instance)
id                                                    
src                └────┘   └────┘   └────────┘  └────────┘   └───┘       └────────────┘
typ             └────┘  └────┘  └────────┘  └────────┘  └───┘       └────────────┘
doc                └────┘   └────┘   └────────┘  └────────┘   └───┘       └────────────┘
txt                └────┘   └────┘   └────────┘  └────────┘   └───┘       └────────────┘
par                └────┘   └────┘   └────────┘  └────────┘   └───┘       └────────────┘
pid                                     └──┘                  
st              └────────┘└───────┘└──────────┘└───────────┘└─────┘└┘    └─────────────┘
137  
138  /-- The trivial groupoid, containing only the identity (and maps with empty source, as this is
139  necessary from the definition) -/
140  def id_groupoid (H : Type u) [topological_space H] : structure_groupoid H :=
id                                 └───────────────┘     └────────────────┘ 
src                                └───────────────┘      └────────────────┘
typ                                └───────────────┘     └────────────────┘ 
doc                                └───────────────┘      └────────────────┘
141  { members := {local_homeomorph.refl H} ∪ {e : local_homeomorph H H | e.source = ∅},
id                └───────────────────┘        └──────────────┘     └─────┘  
src               └───────────────────┘         └──────────────┘        └─────┘  
typ               └───────────────────┘        └──────────────┘     └─────┘  
doc                └───────────────────┘           └──────────────┘
142    comp := λe e' he he', begin
id               └┘ └┘ └─┘
typ              └┘ └┘ └─┘
st                           └─────
143      cases he; simp at he he',
id             └┘
src      └────┘    └────────────┘
typ      └────┘└┘  └────────────┘
doc      └────┘    └────────────┘
txt      └────┘    └────────────┘
par      └────┘    └────────────┘
pid                   └───────┘
st   ───────────────────────────┘└─
144      { simpa [he] },
id                └┘
src        └─────┘  └┘
typ        └─────┘└┘└┘
doc        └─────┘  └┘
txt        └─────┘  └┘
par        └─────┘  └┘
pid               
st   ─────┘└─────────┘└┘
145      { have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _,
id                   └┘ └┘          └──────┘    └────────┘
src        └─────┘  └┘  └───────┘└──────┘└──┘└────────┘└──┘
typ        └─────┘  └┘└┘└───────┘└──────┘└──┘└────────┘└──┘
doc        └─────┘  └┘  └───────┘         └──┘          └──┘
txt        └─────┘      └───────┘         └──┘          └──┘
par        └─────┘      └───────┘         └──┘          └──┘
pid        └───┘└┘      └───────┘         └──┘          └──┘
st   ─────────────────────────────────────────────────────────┘└─
146        rw he at this,
id            └┘
src        └─┘  └──────┘
typ        └─┘└┘└──────┘
doc        └─┘  └──────┘
txt        └─┘  └──────┘
par        └─┘  └──────┘
pid            └──────┘
st   ──────────────────┘└─
147        have : (e ≫ₕ e') ∈ {e : local_homeomorph H H | e.source = ∅} := disjoint_iff.1 this,
id                     └┘       └──────────────┘       └─────┘       └──────────┘   └──┘
src        └─────┘      └┘└──┘└──────────────┘  └─┘ └─────┘└───┘└──────────┘└─┘
typ        └─────┘   └┘└┘└──┘└──────────────┘ └─┘ └─────┘└───┘└──────────┘└─┘└──┘
doc        └─────┘      └┘  └──┘└──────────────┘  └─┘          └───┘            └─┘
txt        └─────┘      └┘  └──┘                  └─┘          └───┘            └─┘
par        └─────┘      └┘  └──┘                  └─┘          └───┘            └─┘
pid        └───┘└┘      └┘  └──┘                  └─┘          └──┘            └─┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
148        exact (mem_union _ _ _).2 (or.inr this) },
id                └───────┘           └────┘ └──┘
src        └────┘ └───────┘└────────┘ └────┘    └┘
typ        └────┘ └───────┘└────────┘ └────┘└──┘└┘
doc        └────┘          └────────┘           └┘
txt        └────┘          └────────┘           └┘
par        └────┘          └────────┘           └┘
pid                       └────────┘           
st   ─────────────────────────────────────────────┘└──
149    end,
st   ────┘
150    inv := λe he, begin
id              └┘
typ             └┘
st                   └─────
151      cases (mem_union _ _ _).1 he with E E,
id              └───────┘          └┘
src      └────┘ └───────┘└────────┘  └───────┘
typ      └────┘ └───────┘└────────┘└┘└───────┘
doc      └────┘          └────────┘  └───────┘
txt      └────┘          └────────┘  └───────┘
par      └────┘          └────────┘  └───────┘
pid                     └────────┘  └───────┘
st   ────────────────────────────────────────┘└─
152      { finish },
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid              
st   ─────┘└─────┘└┘
153      { right,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
154        simpa [e.to_local_equiv.image_source_eq_target.symm] using E },
id                                                                    
src        └─────┘                                            └──────┘ 
typ        └─────┘└──────────────────────────────────────────┘└──────┘
doc        └─────┘                                            └──────┘ 
txt        └─────┘                                            └──────┘ 
par        └─────┘                                            └──────┘ 
pid                                                         └────┘ 
st   ──────────────────────────────────────────────────────────────────┘└──
155    end,
st   ────┘
156    id_mem := mem_union_left _ (mem_insert _ ∅),
id               └────────────┘    └────────┘   
src              └────────────┘    └────────┘   
typ              └────────────┘    └────────┘   
157    locality := λe he, begin
id                   └┘
typ                  └┘
st                        └─────
158      cases e.source.eq_empty_or_nonempty with h h,
id             └───────────────────────────┘
src      └────┘└───────────────────────────┘└───────┘
typ      └────┘└───────────────────────────┘└───────┘
doc      └────┘                             └───────┘
txt      └────┘                             └───────┘
par      └────┘                             └───────┘
pid                                        └───────┘
st   ───────────────────────────────────────────────┘└─
159      { right, exact h },
id                      
src        └───┘  └────┘ 
typ        └───┘  └────┘
doc        └───┘  └────┘ 
txt        └───┘  └────┘ 
par        └───┘  └────┘ 
pid                     
st   ─────┘└───┘└────────┘└┘
160      { left,
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st   ─────────┘└─
161        rcases h with ⟨x, hx⟩,
id                
src        └─────┘ └───────────┘
typ        └─────┘└───────────┘
doc        └─────┘ └───────────┘
txt        └─────┘ └───────────┘
par        └─────┘ └───────────┘
pid               └───────────┘
st   ──────────────────────────┘└─
162        rcases he x hx with ⟨s, open_s, xs, hs⟩,
id                └┘  └┘
src        └─────┘     └───────────────────────┘
typ        └─────┘└┘└┘└───────────────────────┘
doc        └─────┘     └───────────────────────┘
txt        └─────┘     └───────────────────────┘
par        └─────┘     └───────────────────────┘
pid                   └───────────────────────┘
st   ────────────────────────────────────────────┘└─
163        have x's : x ∈ (e.restr s).source,
id                        └─────┘ 
src        └─────────┘   └─────┘ └──────┘
typ        └─────────┘  └─────┘└──────┘
doc        └─────────┘   └─────┘ └──────┘
txt        └─────────┘           └──────┘
par        └─────────┘           └──────┘
pid        └──────┘└─┘           └─────┘
st   ──────────────────────────────────────┘└─
164        { rw [restr_source, interior_eq_of_open open_s],
id               └──────────┘  └─────────────────┘ └────┘
src          └──┘└──────────┘└┘└─────────────────┘      
typ          └──┘└──────────┘└┘└─────────────────┘└────┘
doc          └──┘            └┘                         
txt          └──┘            └┘                         
par          └──┘            └┘                         
pid            └┘            └┘                         
st   ───────┘└──────────────┘└──────────────────────────┘└──
165          exact ⟨hx, xs⟩ },
id                  └┘  └┘
src          └────┘   └┘  └┘
typ          └────┘ └┘└┘└┘└┘
doc          └────┘   └┘  └┘
txt          └────┘   └┘  └┘
par          └────┘   └┘  └┘
pid                  └┘  
st   ──────────────────────┘└┘
166        cases hs,
id               └┘
src        └────┘
typ        └────┘└┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────┘└─
167        { replace hs : local_homeomorph.restr e s = local_homeomorph.refl H,
id                        └────────────────────┘     └───────────────────┘ 
src          └───────────┘└────────────────────┘   └───────────────────┘
typ          └───────────┘└────────────────────┘ └───────────────────┘
doc          └───────────┘└────────────────────┘   └───────────────────┘
txt          └───────────┘                                              
par          └───────────┘                                              
pid                 └─┘└─┘                                              
st   ───────┘└───────────────────────────────────────────────────────────────┘
168            by simpa using hs,
id                            └┘
src               └──────────┘
typ               └──────────┘└┘
doc               └──────────┘
txt               └──────────┘
par               └──────────┘
pid                    └────┘
st                              └─
169          have : (e.restr s).source = univ, by { rw hs, simp },
id                   └─────┘            └──┘          └┘
src          └─────┘ └─────┘ └───────┘ └──┘       └─┘    └───┘
typ          └─────┘ └─────┘└───────┘ └──┘       └─┘└┘  └───┘
doc          └─────┘ └─────┘ └───────┘            └─┘    └───┘
txt          └─────┘         └───────┘            └─┘    └───┘
par          └─────┘         └───────┘            └─┘    └───┘
pid          └───┘└┘         └───────┘                      
st   ───────────────────────────────────────┘     └────┘└─────┘└┘
170          change (e.to_local_equiv).source ∩ interior s = univ at this,
id                   └──────────────┘          └──────┘    └──┘
src          └─────┘ └──────────────┘└───────┘└──────┘  └──┘└──────┘
typ          └─────┘ └──────────────┘└───────┘└──────┘ └──┘└──────┘
doc          └─────┘                 └───────┘ └──────┘      └──────┘
txt          └─────┘                 └───────┘               └──────┘
par          └─────┘                 └───────┘               └──────┘
pid                                 └───────┘               └─────┘
st   ───────────────────────────────────────────────────────────────────┘└─
171          have : univ ⊆ interior s, by { rw ← this, exact inter_subset_right _ _ },
id                  └──┘   └──────┘             └──┘        └────────────────┘
src          └─────┘└──┘ └──────┘        └───┘      └────┘└────────────────┘└───┘
typ          └─────┘└──┘ └──────┘       └───┘└──┘  └────┘└────────────────┘└───┘
doc          └─────┘     └──────┘        └───┘      └────┘                  └───┘
txt          └─────┘                     └───┘      └────┘                  └───┘
par          └─────┘                     └───┘      └────┘                  └───┘
pid          └───┘└┘                       └─┘                             └──┘
st   ───────────────────────────────┘     └────────┘└─────────────────────────────┘└┘
172          have : s = univ, by rwa [interior_eq_of_open open_s, univ_subset_iff] at this,
id                     └──┘          └─────────────────┘ └────┘  └─────────────┘
src          └─────┘  └──┘     └───┘└─────────────────┘      └┘└─────────────┘└───────┘
typ          └─────┘ └──┘     └───┘└─────────────────┘└────┘└┘└─────────────┘└───────┘
doc          └─────┘           └───┘                         └┘               └───────┘
txt          └─────┘           └───┘                         └┘               └───────┘
par          └─────┘           └───┘                         └┘               └───────┘
pid          └───┘└┘              └┘                         └┘               └──────┘
st   ──────────────────────┘          └────────────────────────┘└───────────────┘        └─
173          simpa [this, restr_univ] using hs },
id                  └──┘  └────────┘        └┘
src          └─────┘    └┘└────────┘└──────┘  
typ          └─────┘└──┘└┘└────────┘└──────┘└┘
doc          └─────┘    └┘          └──────┘  
txt          └─────┘    └┘          └──────┘  
par          └─────┘    └┘          └──────┘  
pid                   └┘          └────┘  
st   ─────────────────────────────────────────┘└┘
174        { exfalso,
src          └─────┘
typ          └─────┘
doc          └─────┘
txt          └─────┘
par          └─────┘
st   ──────────────┘└─
175          rw mem_set_of_eq at hs,
id              └───────────┘
src          └─┘└───────────┘└────┘
typ          └─┘└───────────┘└────┘
doc          └─┘             └────┘
txt          └─┘             └────┘
par          └─┘             └────┘
pid                         └────┘
st   ─────────────────────────────┘└─
176          rwa hs at x's } },
id               └┘
src          └──┘  └──────┘
typ          └──┘└┘└──────┘
doc          └──┘  └──────┘
txt          └──┘  └──────┘
par          └──┘  └──────┘
pid               └─────┘
st   ─────────────────────┘└────
177    end,
st   ────┘
178    eq_on_source := λe e' he he'e, begin
id                       └┘ └┘ └──┘
typ                      └┘ └┘ └──┘
st                                    └─────
179      cases he,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
180      { left,
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st   ─────┘└──┘└─
181        have : e = e',
id                   └┘
src        └─────┘  
typ        └─────┘ └┘
doc        └─────┘  
txt        └─────┘  
par        └─────┘  
pid        └───┘└┘  
st   ──────────────────┘└─
182        { refine eq_of_eq_on_source_univ (setoid.symm he'e) _ _;
id                  └─────────────────────┘  └─────────┘ └──┘
src          └─────┘└─────────────────────┘ └─────────┘    └───┘
typ          └─────┘└─────────────────────┘ └─────────┘└──┘└───┘
doc          └─────┘                                       └───┘
txt          └─────┘                                       └───┘
par          └─────┘                                       └───┘
pid                                                       └───┘
st   ───────┘└──────────────────────────────────────────────────────
183          rw set.mem_singleton_iff.1 he ; refl },
id              └───────────────────┘   └┘
src          └─┘└───────────────────┘└─┘    └───┘
typ          └─┘└───────────────────┘└─┘└┘  └───┘
doc          └─┘                     └─┘    └───┘
txt          └─┘                     └─┘    └───┘
par          └─┘                     └─┘    └───┘
pid                                 └─┘        
st   ──────────┘└───────────────────┘└───────────┘└┘
184        rwa ← this },
id               └──┘
src        └────┘    
typ        └────┘└──┘
doc        └────┘    
txt        └────┘    
par        └────┘    
pid           └─┘    
st   ────────────────┘└┘
185      { right,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
186        change (e.to_local_equiv).source = ∅ at he,
id                 └──────────────┘
src        └─────┘ └──────────────┘└───────┘  └────┘
typ        └─────┘ └──────────────┘└───────┘  └────┘
doc        └─────┘                 └───────┘  └────┘
txt        └─────┘                 └───────┘  └────┘
par        └─────┘                 └───────┘  └────┘
pid                               └───────┘  └───┘
st   ───────────────────────────────────────────────┘└─
187        rwa [set.mem_set_of_eq, source_eq_of_eq_on_source he'e] }
id              └───────────────┘  └───────────────────────┘ └──┘
src        └───┘└───────────────┘└┘└───────────────────────┘    └┘
typ        └───┘└───────────────┘└┘└───────────────────────┘└──┘└┘
doc        └───┘                 └┘└───────────────────────┘    └┘
txt        └───┘                 └┘                             └┘
par        └───┘                 └┘                             └┘
pid           └┘                 └┘                             
st   ───────────────────────────┘└──────────────────────────────┘└─
188    end }
st   ────┘
189  
190  /-- Every structure groupoid contains the identity groupoid -/
191  instance : lattice.order_bot (structure_groupoid H) :=
id              └───────────────┘  └────────────────┘ 
src             └───────────────┘  └────────────────┘
typ             └───────────────┘  └────────────────┘ 
doc             └───────────────┘  └────────────────┘
192  { bot    := id_groupoid H,
id               └─────────┘ 
src              └─────────┘
typ              └─────────┘ 
doc              └─────────┘
193    bot_le := begin
st               └─────
194      assume u f hf,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid      └───────────┘
st   ────────────────┘└─
195      change f ∈ {local_homeomorph.refl H} ∪ {e : local_homeomorph H H | e.source = ∅} at hf,
id                                              └──────────────┘       └─────┘  
src      └─────┘ └────────────────────┘ └┘└──┘└──────────────┘  └─┘ └─────┘└─────┘
typ      └─────┘└────────────────────┘ └┘└──┘└──────────────┘ └─┘ └─────┘└─────┘
doc      └─────┘   └────────────────────┘ └┘  └──┘└──────────────┘  └─┘          └─────┘
txt      └─────┘   └────────────────────┘ └┘  └──┘                  └─┘          └─────┘
par      └─────┘   └────────────────────┘ └┘  └──┘                  └─┘          └─────┘
pid               └────────────────────┘ └┘  └──┘                  └─┘          └───┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
196      simp only [singleton_union, mem_set_of_eq, mem_insert_iff] at hf,
id                  └─────────────┘  └───────────┘  └────────────┘
src      └─────────┘└─────────────┘└┘└───────────┘└┘└────────────┘└─────┘
typ      └─────────┘└─────────────┘└┘└───────────┘└┘└────────────┘└─────┘
doc      └─────────┘               └┘             └┘              └─────┘
txt      └─────────┘               └┘             └┘              └─────┘
par      └─────────┘               └┘             └┘              └─────┘
pid          └──┘└┘               └┘             └┘              └───┘
st   ───────────────────────────────────────────────────────────────────┘└─
197      cases hf,
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
198      { rw hf,
id            └┘
src        └─┘
typ        └─┘└┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└───┘└─
199        apply u.id_mem },
src        └────┘        
typ        └────┘        
doc        └────┘        
txt        └────┘        
par        └────┘        
pid                     
st   ────────────────────┘└┘
200      { apply u.locality,
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
201        assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ────────────────┘└─
202        rw [hf, mem_empty_eq] at hx,
id             └┘  └──────────┘
src        └──┘  └┘└──────────┘└─────┘
typ        └──┘└┘└┘└──────────┘└─────┘
doc        └──┘  └┘            └─────┘
txt        └──┘  └┘            └─────┘
par        └──┘  └┘            └─────┘
pid          └┘  └┘            └────┘
st   ───────────┘└────────────┘└────┘└─
203        exact hx.elim }
id               └─────┘
src        └────┘└─────┘
typ        └────┘└─────┘
doc        └────┘       
txt        └────┘       
par        └────┘       
pid                    
st   ───────────────────┘└─
204    end,
st   ────┘
205    ..structure_groupoid.partial_order }
id       └──────────────────────────────┘
src      └──────────────────────────────┘
typ      └──────────────────────────────┘
doc      └──────────────────────────────┘
206  
207  /-- To construct a groupoid, one may consider classes of local homeos such that both the function
208  and its inverse have some property. If this property is stable under composition,
209  one gets a groupoid. `pregroupoid` bundles the properties needed for this construction, with the
210  groupoid of smooth functions with smooth inverses as an application. -/
211  structure pregroupoid (H : Type*) [topological_space H] :=
id                              └───┘   └───────────────┘ 
src                                     └───────────────┘
typ                             └───┘   └───────────────┘ 
doc                                     └───────────────┘
212  (property : (H → H) → (set H) → Prop)
id                      └─┘ 
src                         └─┘
typ                     └─┘ 
213  (comp     : ∀{f g u v}, property f u → property g v → is_open (u ∩ f ⁻¹' v)
id                      └──────┘     └──────┘     └─────┘     └─┘ 
src                                                        └─────┘       └─┘
typ                     └──────┘     └──────┘     └─────┘     └─┘ 
doc                                                        └─────┘        └─┘
214                → property (g ∘ f) (u ∩ f ⁻¹' v))
id                   └──────┘          └─┘ 
src                                        └─┘
typ                  └──────┘          └─┘ 
doc                                          └─┘
215  (id_mem   : property id univ)
id               └──────┘ └┘ └──┘
src                       └┘ └──┘
typ              └──────┘ └┘ └──┘
216  (locality : ∀{f u}, is_open u → (∀x∈u, ∃v, is_open v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u)
id                    └─────┘          └─────┘       └──────┘          └──────┘  
src                      └─────┘              └─────┘                        
typ                   └─────┘          └─────┘       └──────┘          └──────┘  
doc                      └─────┘                └─────┘
217  (congr    : ∀{f g : H → H} {u}, is_open u → (∀x∈u, g x = f x) → property f u → property g u)
id                              └─────┘                 └──────┘     └──────┘  
src                                 └─────┘                
typ                             └─────┘                 └──────┘     └──────┘  
doc                                  └─────┘
218  
219  /-- Construct a groupoid of local homeos for which the map and its inverse have some property,
220  from a pregroupoid asserting that this property is stable under composition. -/
221  def pregroupoid.groupoid (PG : pregroupoid H) : structure_groupoid H :=
id                                  └─────────┘     └────────────────┘ 
src                                 └─────────┘      └────────────────┘
typ                                 └─────────┘     └────────────────┘ 
doc                                 └─────────┘      └────────────────┘
222  { members  := {e : local_homeomorph H H | PG.property e.to_fun e.source ∧ PG.property e.inv_fun e.target},
id                     └──────────────┘     └┘└───────┘ └─────┘ └─────┘  └┘└───────┘ └──────┘ └─────┘
src                    └──────────────┘         └───────┘  └─────┘  └─────┘    └───────┘  └──────┘  └─────┘
typ                    └──────────────┘     └┘└───────┘ └─────┘ └─────┘  └┘└───────┘ └──────┘ └─────┘
doc                     └──────────────┘
223    comp     := λe e' he he', begin
id                   └┘ └┘ └─┘
typ                  └┘ └┘ └─┘
st                               └─────
224      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
225      { apply PG.comp he.1 he'.1,
id               └─────┘ └┘   └─┘
src        └────┘└─────┘  └─┘   └┘
typ        └────┘└─────┘└┘└─┘└─┘└┘
doc        └────┘         └─┘   └┘
txt        └────┘         └─┘   └┘
par        └────┘         └─┘   └┘
pid                      └─┘   └┘
st   ─────┘└──────────────────────┘└─
226        apply e.continuous_to_fun.preimage_open_of_open e.open_source e'.open_source },
id               └───────────────────────────────────────┘ └───────────┘ └────────────┘
src        └────┘└───────────────────────────────────────┘└───────────┘└────────────┘
typ        └────┘└───────────────────────────────────────┘└───────────┘└────────────┘
doc        └────┘                                                                    
txt        └────┘                                                                    
par        └────┘                                                                    
pid                                                                                 
st   ──────────────────────────────────────────────────────────────────────────────────┘└┘
227      { apply PG.comp he'.2 he.2,
id               └─────┘ └─┘   └┘
src        └────┘└─────┘   └─┘  └┘
typ        └────┘└─────┘└─┘└─┘└┘└┘
doc        └────┘          └─┘  └┘
txt        └────┘          └─┘  └┘
par        └────┘          └─┘  └┘
pid                       └─┘  └┘
st   ─────────────────────────────┘└─
228        apply e'.continuous_inv_fun.preimage_open_of_open e'.open_target e.open_target }
id               └─────────────────────────────────────────┘ └────────────┘ └───────────┘
src        └────┘└─────────────────────────────────────────┘└────────────┘└───────────┘
typ        └────┘└─────────────────────────────────────────┘└────────────┘└───────────┘
doc        └────┘                                                                      
txt        └────┘                                                                      
par        └────┘                                                                      
pid                                                                                   
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
229    end,
st   ────┘
230    inv      := λe he, ⟨he.2, he.1⟩,
id                   └┘   └┘   └┘
src                               
typ                  └┘   └┘   └┘
231    id_mem   := ⟨PG.id_mem, PG.id_mem⟩,
id                  └┘└─────┘  └┘└─────┘
src                   └─────┘    └─────┘
typ                 └┘└─────┘  └┘└─────┘
232    locality := λe he, begin
id                   └┘
typ                  └┘
st                        └─────
233      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
234      { apply PG.locality e.open_source (λx xu, _),
id               └─────────┘ └───────────┘
src        └────┘└─────────┘└───────────┘  └──────┘
typ        └────┘└─────────┘└───────────┘  └──────┘
doc        └────┘                          └──────┘
txt        └────┘                          └──────┘
par        └────┘                          └──────┘
pid                                       └──────┘
st   ─────┘└────────────────────────────────────────┘└─
235        rcases he x xu with ⟨s, s_open, xs, hs⟩,
id                └┘  └┘
src        └─────┘     └───────────────────────┘
typ        └─────┘└┘└┘└───────────────────────┘
doc        └─────┘     └───────────────────────┘
txt        └─────┘     └───────────────────────┘
par        └─────┘     └───────────────────────┘
pid                   └───────────────────────┘
st   ────────────────────────────────────────────┘└─
236        refine ⟨s, s_open, xs, _⟩,
id                   └────┘  └┘
src        └─────┘  └┘      └┘  └──┘
typ        └─────┘ └┘└────┘└┘└┘└──┘
doc        └─────┘  └┘      └┘  └──┘
txt        └─────┘  └┘      └┘  └──┘
par        └─────┘  └┘      └┘  └──┘
pid                └┘      └┘  └──┘
st   ──────────────────────────────┘└─
237        convert hs.1,
id                 └┘
src        └──────┘  └┘
typ        └──────┘└┘└┘
doc        └──────┘  └┘
txt        └──────┘  └┘
par        └──────┘  └┘
pid                 └┘
st   ─────────────────┘└─
238        exact (interior_eq_of_open s_open).symm },
id                └─────────────────┘ └────┘
src        └────┘ └─────────────────┘      └─────┘
typ        └────┘ └─────────────────┘└────┘└─────┘
doc        └────┘                          └─────┘
txt        └────┘                          └─────┘
par        └────┘                          └─────┘
pid                                       └───┘└┘
st   ─────────────────────────────────────────────┘└┘
239      { apply PG.locality e.open_target (λx xu, _),
id               └─────────┘ └───────────┘
src        └────┘└─────────┘└───────────┘  └──────┘
typ        └────┘└─────────┘└───────────┘  └──────┘
doc        └────┘                          └──────┘
txt        └────┘                          └──────┘
par        └────┘                          └──────┘
pid                                       └──────┘
st   ───────────────────────────────────────────────┘└─
240        rcases he (e.inv_fun x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩,
id                └┘  └───────┘    └──────────┘ └┘
src        └─────┘   └───────┘ └┘ └──────────┘  └────────────────────────┘
typ        └─────┘└┘ └───────┘└┘ └──────────┘└┘└────────────────────────┘
doc        └─────┘             └┘               └────────────────────────┘
txt        └─────┘             └┘               └────────────────────────┘
par        └─────┘             └┘               └────────────────────────┘
pid                           └┘               └────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
241        refine ⟨e.target ∩ e.inv_fun ⁻¹' s, _, ⟨xu, xs⟩, _⟩,
id                 └──────┘  └───────┘ └─┘       └┘  └┘
src        └─────┘ └──────┘└───────┘└─┘ └───┘   └┘  └───┘
typ        └─────┘ └──────┘└───────┘└─┘└───┘ └┘└┘└┘└───┘
doc        └─────┘                   └─┘ └───┘   └┘  └───┘
txt        └─────┘                       └───┘   └┘  └───┘
par        └─────┘                       └───┘   └┘  └───┘
pid                                     └───┘   └┘  └───┘
st   ────────────────────────────────────────────────────────┘└─
242        { exact continuous_on.preimage_open_of_open e.continuous_inv_fun e.open_target s_open },
id                 └─────────────────────────────────┘ └──────────────────┘ └───────────┘ └────┘
src          └────┘└─────────────────────────────────┘└──────────────────┘└───────────┘      
typ          └────┘└─────────────────────────────────┘└──────────────────┘└───────────┘└────┘
doc          └────┘                                                                          
txt          └────┘                                                                          
par          └────┘                                                                          
pid                                                                                         
st   ───────┘└──────────────────────────────────────────────────────────────────────────────────┘└┘
243        { rw [← inter_assoc, inter_self],
id                 └─────────┘  └────────┘
src          └────┘└─────────┘└┘└────────┘
typ          └────┘└─────────┘└┘└────────┘
doc          └────┘           └┘          
txt          └────┘           └┘          
par          └────┘           └┘          
pid            └──┘           └┘          
st   ────────────────────────┘└──────────┘└──
244          convert hs.2,
id                   └┘
src          └──────┘  └┘
typ          └──────┘└┘└┘
doc          └──────┘  └┘
txt          └──────┘  └┘
par          └──────┘  └┘
pid                   └┘
st   ───────────────────┘└─
245          exact (interior_eq_of_open s_open).symm } },
id                  └─────────────────┘ └────┘
src          └────┘ └─────────────────┘      └─────┘
typ          └────┘ └─────────────────┘└────┘└─────┘
doc          └────┘                          └─────┘
txt          └────┘                          └─────┘
par          └────┘                          └─────┘
pid                                         └───┘└┘
st   ───────────────────────────────────────────────┘└────
246    end,
st   ────┘
247    eq_on_source := λe e' he ee', begin
id                       └┘ └┘ └─┘
typ                      └┘ └┘ └─┘
st                                   └─────
248      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
249      { apply PG.congr e'.open_source ee'.2,
id               └──────┘ └────────────┘ └─┘
src        └────┘└──────┘└────────────┘   └┘
typ        └────┘└──────┘└────────────┘└─┘└┘
doc        └────┘                         └┘
txt        └────┘                         └┘
par        └────┘                         └┘
pid                                      └┘
st   ─────┘└─────────────────────────────────┘└─
250        simp only [ee'.1, he.1] },
id                    └─┘    └┘
src        └─────────┘   └──┘  └──┘
typ        └─────────┘└─┘└──┘└┘└──┘
doc        └─────────┘   └──┘  └──┘
txt        └─────────┘   └──┘  └──┘
par        └─────────┘   └──┘  └──┘
pid            └──┘└┘   └──┘  └─┘
st   ─────────────────────────────┘└┘
251      { have A := eq_on_source_symm ee',
id                   └───────────────┘ └─┘
src        └────────┘└───────────────┘
typ        └────────┘└───────────────┘└─┘
doc        └────────┘└───────────────┘
txt        └────────┘                 
par        └────────┘                 
pid        └────┘└─┘                 
st   ────────────────────────────────────┘└─
252        apply PG.congr e'.symm.open_source A.2,
id               └──────┘ └─────────────────┘ 
src        └────┘└──────┘└─────────────────┘ └┘
typ        └────┘└──────┘└─────────────────┘└┘
doc        └────┘        └─────────────────┘ └┘
txt        └────┘                            └┘
par        └────┘                            └┘
pid                                         └┘
st   ───────────────────────────────────────────┘└─
253        convert he.2,
id                 └┘
src        └──────┘  └┘
typ        └──────┘└┘└┘
doc        └──────┘  └┘
txt        └──────┘  └┘
par        └──────┘  └┘
pid                 └┘
st   ─────────────────┘└─
254        rw A.1,
id            
src        └─┘ └┘
typ        └─┘└┘
doc        └─┘ └┘
txt        └─┘ └┘
par        └─┘ └┘
pid           └┘
st   ───────────┘└─
255        refl }
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└─
256    end }
st   ────┘
257  
258  lemma mem_groupoid_of_pregroupoid (PG : pregroupoid H) (e : local_homeomorph H H) :
id                                           └─────────┘        └──────────────┘  
src                                          └─────────┘         └──────────────┘
typ                                          └─────────┘        └──────────────┘  
doc                                          └─────────┘         └──────────────┘
259    e ∈ PG.groupoid ↔ PG.property e.to_fun e.source ∧ PG.property e.inv_fun e.target :=
id       └┘└───────┘  └┘└───────┘ └─────┘ └─────┘  └┘└───────┘ └──────┘ └─────┘
src         └───────┘    └───────┘  └─────┘  └─────┘    └───────┘  └──────┘  └─────┘
typ      └┘└───────┘  └┘└───────┘ └─────┘ └─────┘  └┘└───────┘ └──────┘ └─────┘
doc          └───────┘
260  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
261  
262  lemma groupoid_of_pregroupoid_le (PG₁ PG₂ : pregroupoid H)
id                                               └─────────┘ 
src                                              └─────────┘
typ                                              └─────────┘ 
doc                                              └─────────┘
263    (h : ∀f s, PG₁.property f s → PG₂.property f s) :
id              └─┘└───────┘     └─┘└───────┘  
src                  └───────┘          └───────┘
typ             └─┘└───────┘     └─┘└───────┘  
264    PG₁.groupoid ≤ PG₂.groupoid :=
id     └─┘└───────┘  └─┘└───────┘
src       └───────┘     └───────┘
typ    └─┘└───────┘  └─┘└───────┘
doc       └───────┘      └───────┘
265  begin
st   └─────
266    assume e he,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
267    rw mem_groupoid_of_pregroupoid at he ⊢,
id        └─────────────────────────┘
src    └─┘└─────────────────────────┘└──────┘
typ    └─┘└─────────────────────────┘└──────┘
doc    └─┘                           └──────┘
txt    └─┘                           └──────┘
par    └─┘                           └──────┘
pid                                 └──────┘
st   ───────────────────────────────────────┘└─
268    exact ⟨h _ _ he.1, h _ _ he.2⟩
id                             └┘
src    └────┘  └───┘  └──┘ └───┘  └──┘
typ    └────┘  └───┘  └──┘└───┘└┘└──┘
doc    └────┘  └───┘  └──┘ └───┘  └──┘
txt    └────┘  └───┘  └──┘ └───┘  └──┘
par    └────┘  └───┘  └──┘ └───┘  └──┘
pid           └───┘  └──┘ └───┘  └─┘
st   ────────────────────────────────┘
269  end
st   └─┘
270  
271  lemma mem_pregroupoid_of_eq_on_source (PG : pregroupoid H) {e e' : local_homeomorph H H}
id                                               └─────────┘           └──────────────┘  
src                                              └─────────┘            └──────────────┘
typ                                              └─────────┘           └──────────────┘  
doc                                              └─────────┘            └──────────────┘
272    (he' : e ≈ e') (he : PG.property e.to_fun e.source) :
id              └┘        └┘└───────┘ └─────┘ └─────┘
src                          └───────┘  └─────┘  └─────┘
typ             └┘        └┘└───────┘ └─────┘ └─────┘
273    PG.property e'.to_fun e'.source :=
id     └┘└───────┘ └┘└─────┘ └┘└─────┘
src      └───────┘   └─────┘   └─────┘
typ    └┘└───────┘ └┘└─────┘ └┘└─────┘
274  begin
st   └─────
275    rw ← he'.1,
id          └─┘
src    └───┘   └┘
typ    └───┘└─┘└┘
doc    └───┘   └┘
txt    └───┘   └┘
par    └───┘   └┘
pid      └─┘   └┘
st   ───────────┘└─
276    exact PG.congr e.open_source (λx hx, (he'.2 x hx).symm) he,
id           └──────┘ └───────────┘          └─┘               └┘
src    └────┘└──────┘└───────────┘  └────┘    └─┘   └──────┘
typ    └────┘└──────┘└───────────┘  └────┘ └─┘└─┘   └──────┘└┘
doc    └────┘                       └────┘    └─┘   └──────┘
txt    └────┘                       └────┘    └─┘   └──────┘
par    └────┘                       └────┘    └─┘   └──────┘
pid                                └────┘    └─┘   └──────┘
st   ───────────────────────────────────────────────────────────┘└─
277  end
st   ──┘
278  
279  /-- The groupoid of all local homeomorphisms on a topological space H -/
280  def continuous_groupoid (H : Type*) [topological_space H] : structure_groupoid H :=
id                                        └───────────────┘     └────────────────┘ 
src                                       └───────────────┘      └────────────────┘
typ                                       └───────────────┘     └────────────────┘ 
doc                                       └───────────────┘      └────────────────┘
281  pregroupoid.groupoid
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
doc  └──────────────────┘
282  { property := λf s, true,
id                     └──┘
src                      └──┘
typ                    └──┘
283    comp     := λf g u v hf hg huv, trivial,
id                      └┘ └┘ └─┘  └─────┘
src                                    └─────┘
typ                     └┘ └┘ └─┘  └─────┘
284    id_mem   := trivial,
id                 └─────┘
src                └─────┘
typ                └─────┘
285    locality := λf u u_open h, trivial,
id                    └────┘   └─────┘
src                               └─────┘
typ                   └────┘   └─────┘
286    congr    := λf g u u_open hcongr hf, trivial }
id                     └────┘ └────┘ └┘  └─────┘
src                                         └─────┘
typ                    └────┘ └────┘ └┘  └─────┘
287  
288  /-- Every structure groupoid is contained in the groupoid of all local homeomorphisms -/
289  instance : lattice.order_top (structure_groupoid H) :=
id              └───────────────┘  └────────────────┘ 
src             └───────────────┘  └────────────────┘
typ             └───────────────┘  └────────────────┘ 
doc             └───────────────┘  └────────────────┘
290  { top    := continuous_groupoid H,
id               └─────────────────┘ 
src              └─────────────────┘
typ              └─────────────────┘ 
doc              └─────────────────┘
291    le_top := λ u f hf, by { split; exact dec_trivial },
id                   └┘                    └─────────┘
src                             └───┘  └────┘└─────────┘
typ                  └┘       └───┘  └────┘└─────────┘
doc                             └───┘  └────┘└─────────┘
txt                             └───┘  └────┘           
par                             └───┘  └────┘           
pid                                                    
st                           └──────────────────────────┘└┘
292    ..structure_groupoid.partial_order }
id       └──────────────────────────────┘
src      └──────────────────────────────┘
typ      └──────────────────────────────┘
doc      └──────────────────────────────┘
293  
294  end groupoid
295  
296  /-- A manifold is a topological space endowed with an atlas, i.e., a set of local homeomorphisms
297  taking value in a model space H, called charts, such that the domains of the charts cover the whole
298  space. We express the covering property by chosing for each x a member `chart_at x` of the atlas
299  containing x in its source: in the smooth case, this is convenient to construct the tangent bundle
300  in an efficient way.
301  The model space is written as an explicit parameter as there can be several model spaces for a
302  given topological space. For instance, a complex manifold (modelled over ℂ^n) will also be seen
303  sometimes as a real manifold over ℝ^(2n).
304  -/
305  class manifold (H : Type*) [topological_space H] (M : Type*) [topological_space M] :=
id                       └───┘   └───────────────┘        └───┘   └───────────────┘ 
src                              └───────────────┘                 └───────────────┘
typ                      └───┘   └───────────────┘        └───┘   └───────────────┘ 
doc                              └───────────────┘                 └───────────────┘
306  (atlas            : set (local_homeomorph M H))
id                       └─┘  └──────────────┘  
src                      └─┘  └──────────────┘
typ                      └─┘  └──────────────┘  
doc                           └──────────────┘
307  (chart_at         : M → local_homeomorph M H)
id                         └──────────────┘  
src                          └──────────────┘
typ                        └──────────────┘  
doc                          └──────────────┘
308  (mem_chart_source : ∀x, x ∈ (chart_at x).source)
id                             └──────┘  └────┘
src                                         └────┘
typ                            └──────┘  └────┘
309  (chart_mem_atlas  : ∀x, chart_at x ∈ atlas)
id                          └──────┘   └───┘
src                                     
typ                         └──────┘   └───┘
310  
311  export manifold
312  attribute [simp] mem_chart_source chart_mem_atlas
id                    └──────────────┘ └─────────────┘
src                   └──────────────┘ └─────────────┘
typ                   └──────────────┘ └─────────────┘
doc             └──┘
313  
314  section manifold
315  
316  /-- Any space is a manifold modelled over itself, by just using the identity chart -/
317  instance manifold_model_space (H : Type*) [topological_space H] : manifold H H :=
id                                              └───────────────┘     └──────┘  
src                                             └───────────────┘      └──────┘
typ                                             └───────────────┘     └──────┘  
doc                                             └───────────────┘      └──────┘
318  { atlas            := {local_homeomorph.refl H},
id                         └───────────────────┘ 
src                        └───────────────────┘
typ                        └───────────────────┘ 
doc                         └───────────────────┘
319    chart_at         := λx, local_homeomorph.refl H,
id                            └───────────────────┘ 
src                            └───────────────────┘
typ                           └───────────────────┘ 
doc                            └───────────────────┘
320    mem_chart_source := λx, mem_univ x,
id                            └──────┘ 
src                            └──────┘
typ                           └──────┘ 
321    chart_mem_atlas  := λx, mem_singleton _ }
id                            └───────────┘
src                            └───────────┘
typ                           └───────────┘
322  
323  /-- In the trivial manifold structure of a space modelled over itself through the identity, the
324  atlas members are just the identity -/
325  @[simp] lemma model_space_atlas {H : Type*} [topological_space H] {e : local_homeomorph H H} :
id                                                └───────────────┘        └──────────────┘  
src                                               └───────────────┘         └──────────────┘
typ                                               └───────────────┘        └──────────────┘  
doc    └──┘                                       └───────────────┘         └──────────────┘
326    e ∈ atlas H H ↔ e = local_homeomorph.refl H :=
id       └───┘      └───────────────────┘ 
src       └───┘         └───────────────────┘
typ      └───┘      └───────────────────┘ 
doc                        └───────────────────┘
327  by simp [atlas, manifold.atlas]
src     └────┘     └┘              └─
typ     └────┘     └┘              └─
doc     └────┘     └┘              └─
txt     └────┘     └┘              └─
par     └────┘     └┘              └─
pid              └┘              
st     └─────────────────────────────
328  
src  
typ  
doc  
txt  
par  
pid  
st   
329  /-- In the model space, chart_at is always the identity -/
330  @[simp] lemma chart_at_model_space_eq {H : Type*} [topological_space H] {x : H} :
id                                                      └───────────────┘        
src                                                     └───────────────┘
typ                                                     └───────────────┘        
doc    └──┘                                             └───────────────┘
331    chart_at H x = local_homeomorph.refl H :=
id     └──────┘    └───────────────────┘ 
src    └──────┘      └───────────────────┘
typ    └──────┘    └───────────────────┘ 
doc                   └───────────────────┘
332  by simpa using chart_mem_atlas H x
id                  └─────────────┘  
src     └──────────┘└─────────────┘  
typ     └──────────┘└─────────────┘
doc     └──────────┘                 
txt     └──────────┘                 
par     └──────────┘                 
pid          └────┘                 
st     └────────────────────────────────
333  
src  
typ  
doc  
txt  
par  
pid  
st   
334  end manifold
335  
336  /-- Sometimes, one may want to construct a manifold structure on a space which does not yet have
337  a topological structure, where the topology would come from the charts. For this, one needs charts
338  that are only local equivs, and continuity properties for their composition.
339  This is formalised in `manifold_core`. -/
340  structure manifold_core (H : Type*) [topological_space H] (M : Type*) :=
id                                └───┘   └───────────────┘        └───┘
src                                       └───────────────┘
typ                               └───┘   └───────────────┘        └───┘
doc                                       └───────────────┘
341  (atlas            : set (local_equiv M H))
id                       └─┘  └─────────┘  
src                      └─┘  └─────────┘
typ                      └─┘  └─────────┘  
doc                           └─────────┘
342  (chart_at         : M → local_equiv M H)
id                         └─────────┘  
src                          └─────────┘
typ                        └─────────┘  
doc                          └─────────┘
343  (mem_chart_source : ∀x, x ∈ (chart_at x).source)
id                             └──────┘  └────┘
src                                         └────┘
typ                            └──────┘  └────┘
344  (chart_mem_atlas  : ∀x, chart_at x ∈ atlas)
id                          └──────┘   └───┘
src                                     
typ                         └──────┘   └───┘
345  (open_source : ∀e e' : local_equiv M H, e ∈ atlas → e' ∈ atlas → is_open (e.symm.trans e').source)
id                         └─────────┘      └───┘   └┘  └───┘   └─────┘  └───┘└────┘ └┘ └────┘
src                         └─────────┘                             └─────┘   └───┘└────┘    └────┘
typ                        └─────────┘      └───┘   └┘  └───┘   └─────┘  └───┘└────┘ └┘ └────┘
doc                         └─────────┘                               └─────┘   └───┘└────┘
346  (continuous_to_fun : ∀e e' : local_equiv M H, e ∈ atlas → e' ∈ atlas →
id                               └─────────┘      └───┘   └┘  └───┘
src                               └─────────┘                    
typ                              └─────────┘      └───┘   └┘  └───┘
doc                               └─────────┘
347                         continuous_on (e.symm.trans e').to_fun (e.symm.trans e').source)
id                          └───────────┘  └───┘└────┘ └┘ └────┘   └───┘└────┘ └┘ └────┘
src                         └───────────┘   └───┘└────┘    └────┘    └───┘└────┘    └────┘
typ                         └───────────┘  └───┘└────┘ └┘ └────┘   └───┘└────┘ └┘ └────┘
doc                         └───────────┘   └───┘└────┘              └───┘└────┘
348  
349  namespace manifold_core
350  
351  variables [topological_space H] (c : manifold_core H M) {e : local_equiv M H}
id             └───────────────┘         └───────────┘           └─────────┘
src             └───────────────┘         └───────────┘           └─────────┘
typ            └───────────────┘         └───────────┘           └─────────┘
doc             └───────────────┘         └───────────┘           └─────────┘
352  
353  /-- Topology generated by a set of charts on a Type. -/
354  protected def to_topological_space : topological_space M :=
id                                        └───────────────┘ 
src                                       └───────────────┘
typ                                       └───────────────┘ 
doc                                       └───────────────┘
355  topological_space.generate_from $ ⋃ (e : local_equiv M H) (he : e ∈ c.atlas)
id   └─────────────────────────────┘         └─────────┘            └────┘
src  └─────────────────────────────┘         └─────────┘                └────┘
typ  └─────────────────────────────┘         └─────────┘            └────┘
doc  └─────────────────────────────┘         └─────────┘
356    (s : set H) (s_open : is_open s), {e.to_fun ⁻¹' s ∩ e.source}
id          └─┘             └─────┘   └─────┘ └─┘   └─────┘
src         └─┘              └─────┘     └─────┘ └─┘     └─────┘
typ         └─┘             └─────┘   └─────┘ └─┘   └─────┘
doc                          └─────┘              └─┘
357  
358  lemma open_source' (he : e ∈ c.atlas) : @is_open M c.to_topological_space e.source :=
id                              └────┘     └─────┘  └───────────────────┘ └─────┘
src                               └────┘     └─────┘    └───────────────────┘  └─────┘
typ                             └────┘     └─────┘  └───────────────────┘ └─────┘
doc                                           └─────┘    └───────────────────┘
359  begin
st   └─────
360    apply topological_space.generate_open.basic,
id           └───────────────────────────────────┘
src    └────┘└───────────────────────────────────┘
typ    └────┘└───────────────────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────────────────────────────┘└─
361    simp only [exists_prop, mem_Union, mem_singleton_iff],
id                └─────────┘  └───────┘  └───────────────┘
src    └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘
typ    └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘
doc    └─────────┘           └┘         └┘                 
txt    └─────────┘           └┘         └┘                 
par    └─────────┘           └┘         └┘                 
pid        └──┘└┘           └┘         └┘                 
st   ──────────────────────────────────────────────────────┘└─
362    refine ⟨e, he, univ, is_open_univ, _⟩,
id               └┘  └──┘  └──────────┘
src    └─────┘  └┘  └┘└──┘└┘└──────────┘└──┘
typ    └─────┘ └┘└┘└┘└──┘└┘└──────────┘└──┘
doc    └─────┘  └┘  └┘    └┘            └──┘
txt    └─────┘  └┘  └┘    └┘            └──┘
par    └─────┘  └┘  └┘    └┘            └──┘
pid            └┘  └┘    └┘            └──┘
st   ──────────────────────────────────────┘└─
363    simp only [set.univ_inter, set.preimage_univ]
id                └────────────┘  └───────────────┘
src    └─────────┘└────────────┘└┘└───────────────┘└┘
typ    └─────────┘└────────────┘└┘└───────────────┘└┘
doc    └─────────┘              └┘                 └┘
txt    └─────────┘              └┘                 └┘
par    └─────────┘              └┘                 └┘
pid        └──┘└┘              └┘                 
st   ───────────────────────────────────────────────┘
364  end
st   └─┘
365  
366  lemma open_target (he : e ∈ c.atlas) : is_open e.target :=
id                             └────┘    └─────┘ └─────┘
src                              └────┘    └─────┘  └─────┘
typ                            └────┘    └─────┘ └─────┘
doc                                         └─────┘
367  begin
st   └─────
368    have E : e.target ∩ e.inv_fun ⁻¹' e.source = e.target :=
id                        └───────┘ └─┘ └──────┘  └──────┘
src    └───────┘        └───────┘└─┘└──────┘└──────┘└───
typ    └───────┘        └───────┘└─┘└──────┘└──────┘└───
doc    └───────┘                  └─┘                 └───
txt    └───────┘                                      └───
par    └───────┘                                      └───
pid    └────┘└─┘                                      └───
st   ───────────────────────────────────────────────────────────
369    subset.antisymm (inter_subset_left _ _) (λx hx, ⟨hx,
id     └─────────────┘  └───────────────┘
src  ─┘└─────────────┘ └───────────────┘└────┘  └────┘   └─
typ  ─┘└─────────────┘ └───────────────┘└────┘  └────┘   └─
doc  ─┘                                 └────┘  └────┘   └─
txt  ─┘                                 └────┘  └────┘   └─
par  ─┘                                 └────┘  └────┘   └─
pid  ─┘                                 └────┘  └────┘   └─
st   ───────────────────────────────────────────────────────
370      local_equiv.target_subset_preimage_source _ hx⟩),
id       └───────────────────────────────────────┘
src  ───┘└───────────────────────────────────────┘└─┘  └┘
typ  ───┘└───────────────────────────────────────┘└─┘  └┘
doc  ───┘                                         └─┘  └┘
txt  ───┘                                         └─┘  └┘
par  ───┘                                         └─┘  └┘
pid  ───┘                                         └─┘  └┘
st   ───────────────────────────────────────────────────┘└─
371    simpa [local_equiv.trans_source, E] using c.open_source e e he he
id            └──────────────────────┘          └───────────┘       └┘
src    └─────┘└──────────────────────┘└┘ └──────┘└───────────┘      
typ    └─────┘└──────────────────────┘└┘└──────┘└───────────┘   └┘
doc    └─────┘                        └┘ └──────┘                   
txt    └─────┘                        └┘ └──────┘                   
par    └─────┘                        └┘ └──────┘                   
pid                                 └┘ └────┘                   
st   ───────────────────────────────────────────────────────────────────┘
372  end
st   └─┘
373  
374  def local_homeomorph (e : local_equiv M H) (he : e ∈ c.atlas) :
id                             └─────────┘            └────┘
src                            └─────────┘                └────┘
typ                            └─────────┘            └────┘
doc                            └─────────┘
375    @local_homeomorph M H c.to_topological_space _ :=
id      └──────────────┘   └───────────────────┘
src     └──────────────┘      └───────────────────┘
typ     └──────────────┘   └───────────────────┘
doc     └──────────────┘      └───────────────────┘
376  { open_source := by convert c.open_source' he,
id                               └────────────┘ └┘
src                      └──────┘└────────────┘
typ                      └──────┘└────────────┘└┘
doc                      └──────┘              
txt                      └──────┘              
par                      └──────┘              
pid                                           
st                      └────────────────────────┘
377    open_target := by convert c.open_target he,
id                               └───────────┘ └┘
src                      └──────┘└───────────┘
typ                      └──────┘└───────────┘└┘
doc                      └──────┘             
txt                      └──────┘             
par                      └──────┘             
pid                                          
st                      └───────────────────────┘
378    continuous_to_fun := begin
st                          └─────
379      letI : topological_space M := c.to_topological_space,
id              └───────────────┘     └────────────────────┘
src      └─────┘└───────────────┘ └──┘└────────────────────┘
typ      └─────┘└───────────────┘└──┘└────────────────────┘
doc      └─────┘└───────────────┘ └──┘└────────────────────┘
txt      └─────┘                  └──┘
par      └─────┘                  └──┘
pid          └┘                  └──┘
st   ───────────────────────────────────────────────────────┘└─
380      rw continuous_on_open_iff (c.open_source' he),
id          └────────────────────┘  └────────────┘ └┘
src      └─┘└────────────────────┘ └────────────┘  
typ      └─┘└────────────────────┘ └────────────┘└┘
doc      └─┘                                       
txt      └─┘                                       
par      └─┘                                       
pid                                               
st   ────────────────────────────────────────────────┘└─
381      assume s s_open,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid      └─────────────┘
st   ──────────────────┘└─
382      rw inter_comm,
id          └────────┘
src      └─┘└────────┘
typ      └─┘└────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────────┘└─
383      apply topological_space.generate_open.basic,
id             └───────────────────────────────────┘
src      └────┘└───────────────────────────────────┘
typ      └────┘└───────────────────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────────────────────┘└─
384      simp only [exists_prop, mem_Union, mem_singleton_iff],
id                  └─────────┘  └───────┘  └───────────────┘
src      └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘
typ      └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘
doc      └─────────┘           └┘         └┘                 
txt      └─────────┘           └┘         └┘                 
par      └─────────┘           └┘         └┘                 
pid          └──┘└┘           └┘         └┘                 
st   ────────────────────────────────────────────────────────┘└─
385      exact ⟨e, he, ⟨s, s_open, rfl⟩⟩
id                └┘     └────┘  └─┘
src      └────┘  └┘  └┘  └┘      └┘└─┘└──
typ      └────┘ └┘└┘└┘ └┘└────┘└┘└─┘└──
doc      └────┘  └┘  └┘  └┘      └┘   └──
txt      └────┘  └┘  └┘  └┘      └┘   └──
par      └────┘  └┘  └┘  └┘      └┘   └──
pid             └┘  └┘  └┘      └┘   └┘
st   ────────────────────────────────────
386    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
387    continuous_inv_fun := begin
st                           └─────
388      letI : topological_space M := c.to_topological_space,
id              └───────────────┘     └────────────────────┘
src      └─────┘└───────────────┘ └──┘└────────────────────┘
typ      └─────┘└───────────────┘└──┘└────────────────────┘
doc      └─────┘└───────────────┘ └──┘└────────────────────┘
txt      └─────┘                  └──┘
par      └─────┘                  └──┘
pid          └┘                  └──┘
st   ───────────────────────────────────────────────────────┘└─
389      apply continuous_on_open_of_generate_from (c.open_target he),
id             └─────────────────────────────────┘  └───────────┘ └┘
src      └────┘└─────────────────────────────────┘ └───────────┘  
typ      └────┘└─────────────────────────────────┘ └───────────┘└┘
doc      └────┘                                                   
txt      └────┘                                                   
par      └────┘                                                   
pid                                                              
st   ───────────────────────────────────────────────────────────────┘└─
390      assume t ht,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
391      simp only [exists_prop, mem_Union, mem_singleton_iff] at ht,
id                  └─────────┘  └───────┘  └───────────────┘
src      └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘└─────┘
typ      └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘└─────┘
doc      └─────────┘           └┘         └┘                 └─────┘
txt      └─────────┘           └┘         └┘                 └─────┘
par      └─────────┘           └┘         └┘                 └─────┘
pid          └──┘└┘           └┘         └┘                 └───┘
st   ──────────────────────────────────────────────────────────────┘└─
392      rcases ht with ⟨e', e'_atlas, s, s_open, ts⟩,
id              └┘
src      └─────┘  └─────────────────────────────────┘
typ      └─────┘└┘└─────────────────────────────────┘
doc      └─────┘  └─────────────────────────────────┘
txt      └─────┘  └─────────────────────────────────┘
par      └─────┘  └─────────────────────────────────┘
pid              └─────────────────────────────────┘
st   ───────────────────────────────────────────────┘└─
393      rw ts,
id          └┘
src      └─┘
typ      └─┘└┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────┘└─
394      let f := e.symm.trans e',
id                └──────────┘ └┘
src      └───────┘└──────────┘
typ      └───────┘└──────────┘└┘
doc      └───────┘└──────────┘
txt      └───────┘            
par      └───────┘            
pid      └───┘└─┘            
st   ───────────────────────────┘└─
395      have : is_open (f.to_fun ⁻¹' s ∩ f.source),
id              └─────┘  └──────┘ └─┘   └──────┘
src      └─────┘└─────┘ └──────┘└─┘ └──────┘
typ      └─────┘└─────┘ └──────┘└─┘└──────┘
doc      └─────┘└─────┘         └─┘          
txt      └─────┘                             
par      └─────┘                             
pid      └───┘└┘                             
st   ─────────────────────────────────────────────┘
396        by simpa [inter_comm] using (continuous_on_open_iff (c.open_source e e' he e'_atlas)).1
id                   └────────┘         └────────────────────┘  └───────────┘
src           └─────┘└────────┘└──────┘ └────────────────────┘ └───────────┘             └────
typ           └─────┘└────────┘└──────┘ └────────────────────┘ └───────────┘             └────
doc           └─────┘          └──────┘                                                  └────
txt           └─────┘          └──────┘                                                  └────
par           └─────┘          └──────┘                                                  └────
pid                          └────┘                                                  └────
397          (c.continuous_to_fun e e' he e'_atlas) s s_open,
id            └─────────────────┘  └┘ └┘ └──────┘   └────┘
src  ───────┘ └─────────────────┘             └┘ 
typ  ───────┘ └─────────────────┘└┘└┘└──────┘└┘└────┘
doc  ───────┘                                 └┘ 
txt  ───────┘                                 └┘ 
par  ───────┘                                 └┘ 
pid  ───────┘                                 └┘ 
st                                                          └─
398      have A : e'.to_fun ∘ e.inv_fun ⁻¹' s ∩ (e.target ∩ e.inv_fun ⁻¹' e'.source) =
id                                                                                  
src      └───────┘                                                      └┘
typ      └───────┘                                                      └┘
doc      └───────┘                                                       └┘ 
txt      └───────┘                                                       └┘ 
par      └───────┘                                                       └┘ 
pid      └────┘└─┘                                                       └┘ 
st   ──────────────────────────────────────────────────────────────────────────────────
399               e.target ∩ (e'.to_fun ∘ e.inv_fun ⁻¹' s ∩ e.inv_fun ⁻¹' e'.source),
id                └──────┘    └───────┘                    └───────┘     └───────┘
src  ────────────┘└──────┘  └───────┘               └───────┘   └───────┘
typ  ────────────┘└──────┘  └───────┘              └───────┘   └───────┘
doc  ────────────┘                                                       
txt  ────────────┘                                                       
par  ────────────┘                                                       
pid  ────────────┘                                                       
st   ──────────────────────────────────────────────────────────────────────────────┘
400        by { rw [← inter_assoc, ← inter_assoc], congr' 1, exact inter_comm _ _ },
id                    └─────────┘    └─────────┘                   └────────┘
src             └────┘└─────────┘└──┘└─────────┘  └──────┘  └────┘└────────┘└───┘
typ             └────┘└─────────┘└──┘└─────────┘  └──────┘  └────┘└────────┘└───┘
doc             └────┘           └──┘             └──────┘  └────┘          └───┘
txt             └────┘           └──┘             └──────┘  └────┘          └───┘
par             └────┘           └──┘             └──────┘  └────┘          └───┘
pid               └──┘           └──┘                                    └──┘
st            └────────────────┘└─────────────┘└─────────┘└─────────────────────┘└┘
401      simpa [local_equiv.trans_source, preimage_inter, preimage_comp.symm, A] using this
id              └──────────────────────┘  └────────────┘                              └──┘
src      └─────┘└──────────────────────┘└┘└────────────┘└┘                  └┘ └──────┘    
typ      └─────┘└──────────────────────┘└┘└────────────┘└┘└────────────────┘└┘└──────┘└──┘
doc      └─────┘                        └┘              └┘                  └┘ └──────┘    
txt      └─────┘                        └┘              └┘                  └┘ └──────┘    
par      └─────┘                        └┘              └┘                  └┘ └──────┘    
pid                                   └┘              └┘                  └┘ └────┘    
st   ───────────────────────────────────────────────────────────────────────────────────────
402    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
403    ..e }
id       
typ      
404  
405  def to_manifold : @manifold H _ M c.to_topological_space :=
id                      └──────┘     └───────────────────┘
src                     └──────┘        └───────────────────┘
typ                     └──────┘     └───────────────────┘
doc                     └──────┘        └───────────────────┘
406  { atlas := ⋃ (e : local_equiv M H) (he : e ∈ c.atlas), {c.local_homeomorph e he},
id                    └─────────┘            └────┘  └───────────────┘  └┘
src                   └─────────┘                └────┘   └───────────────┘
typ                   └─────────┘            └────┘  └───────────────┘  └┘
doc                   └─────────┘                        
407    chart_at := λx, c.local_homeomorph (c.chart_at x) (c.chart_mem_atlas x),
id                    └───────────────┘  └───────┘    └──────────────┘ 
src                     └───────────────┘   └───────┘      └──────────────┘
typ                   └───────────────┘  └───────┘    └──────────────┘ 
408    mem_chart_source := λx, c.mem_chart_source x,
id                            └───────────────┘ 
src                             └───────────────┘
typ                           └───────────────┘ 
409    chart_mem_atlas := λx, begin
id                         
typ                        
st                            └─────
410      simp only [mem_Union, mem_singleton_iff],
id                  └───────┘  └───────────────┘
src      └─────────┘└───────┘└┘└───────────────┘
typ      └─────────┘└───────┘└┘└───────────────┘
doc      └─────────┘         └┘                 
txt      └─────────┘         └┘                 
par      └─────────┘         └┘                 
pid          └──┘└┘         └┘                 
st   ───────────────────────────────────────────┘└─
411      exact ⟨c.chart_at x, c.chart_mem_atlas x, rfl⟩,
id              └────────┘    └───────────────┘   └─┘
src      └────┘ └────────┘ └┘└───────────────┘ └┘└─┘
typ      └────┘ └────────┘ └┘└───────────────┘└┘└─┘
doc      └────┘            └┘                  └┘   
txt      └────┘            └┘                  └┘   
par      └────┘            └┘                  └┘   
pid                       └┘                  └┘   
st   ─────────────────────────────────────────────────┘└─
412    end }
st   ────┘
413  
414  end manifold_core
415  
416  section has_groupoid
417  variables [topological_space H] [topological_space M] [manifold H M]
id              └───────────────┘     └───────────────┘     └──────┘
src             └───────────────┘     └───────────────┘     └──────┘
typ             └───────────────┘     └───────────────┘     └──────┘
doc             └───────────────┘     └───────────────┘     └──────┘
418  
419  /-- A manifold has an atlas in a groupoid G if the change of coordinates belong to the groupoid -/
420  class has_groupoid {H : Type*} [topological_space H] (M : Type*) [topological_space M]
id                           └───┘   └───────────────┘        └───┘   └───────────────┘ 
src                                  └───────────────┘                 └───────────────┘
typ                          └───┘   └───────────────┘        └───┘   └───────────────┘ 
doc                                  └───────────────┘                 └───────────────┘
421    [manifold H M] (G : structure_groupoid H) : Prop :=
id      └──────┘         └────────────────┘ 
src     └──────┘           └────────────────┘
typ     └──────┘         └────────────────┘ 
doc     └──────┘           └────────────────┘
422  (compatible : ∀{e e' : local_homeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ G)
id                         └──────────────┘       └───┘     └┘  └───┘     └───┘ └┘ └┘  
src                         └──────────────┘          └───┘           └───┘        └───┘ └┘    
typ                        └──────────────┘       └───┘     └┘  └───┘     └───┘ └┘ └┘  
doc                         └──────────────┘                                         └───┘ └┘
423  
424  lemma has_groupoid_of_le {G₁ G₂ : structure_groupoid H} (h : has_groupoid M G₁) (hle : G₁ ≤ G₂) :
id                                     └────────────────┘        └──────────┘  └┘         └┘  └┘
src                                    └────────────────┘         └──────────┘                 
typ                                    └────────────────┘        └──────────┘  └┘         └┘  └┘
doc                                    └────────────────┘         └──────────┘
425    has_groupoid M G₂ :=
id     └──────────┘  └┘
src    └──────────┘
typ    └──────────┘  └┘
doc    └──────────┘
426  ⟨ λ e e' he he', hle ((h.compatible : _) he he') ⟩
id        └┘ └┘ └─┘  └─┘   └─────────┘      └┘ └─┘
src                          └─────────┘
typ       └┘ └┘ └─┘  └─┘   └─────────┘      └┘ └─┘
427  
428  lemma has_groupoid_of_pregroupoid (PG : pregroupoid H)
id                                           └─────────┘ 
src                                          └─────────┘
typ                                          └─────────┘ 
doc                                          └─────────┘
429    (h : ∀{e e' : local_homeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M
id                   └──────────────┘       └───┘     └┘  └───┘  
src                  └──────────────┘          └───┘           └───┘
typ                  └──────────────┘       └───┘     └┘  └───┘  
doc                  └──────────────┘
430      → PG.property (e.symm ≫ₕ e').to_fun (e.symm ≫ₕ e').source) :
id         └┘└───────┘  └───┘ └┘ └┘ └────┘   └───┘ └┘ └┘ └────┘
src          └───────┘   └───┘ └┘    └────┘    └───┘ └┘    └────┘
typ        └┘└───────┘  └───┘ └┘ └┘ └────┘   └───┘ └┘ └┘ └────┘
doc                      └───┘ └┘              └───┘ └┘
431    has_groupoid M (PG.groupoid) :=
id     └──────────┘   └┘└───────┘
src    └──────────┘      └───────┘
typ    └──────────┘   └┘└───────┘
doc    └──────────┘      └───────┘
432  ⟨assume e e' he he', (mem_groupoid_of_pregroupoid PG _).mpr ⟨h he he', h he' he⟩⟩
id            └┘ └┘ └─┘   └─────────────────────────┘ └┘   └─┘    └┘ └─┘   └─┘ └┘
src                        └─────────────────────────┘      └─┘
typ           └┘ └┘ └─┘   └─────────────────────────┘ └┘   └─┘    └┘ └─┘   └─┘ └┘
433  
434  /-- The trivial manifold structure on the model space is compatible with any groupoid -/
435  instance has_groupoid_model_space (H : Type*) [topological_space H] (G : structure_groupoid H) :
id                                                  └───────────────┘        └────────────────┘ 
src                                                 └───────────────┘         └────────────────┘
typ                                                 └───────────────┘        └────────────────┘ 
doc                                                 └───────────────┘         └────────────────┘
436    has_groupoid H G :=
id     └──────────┘  
src    └──────────┘
typ    └──────────┘  
doc    └──────────┘
437  { compatible := λe e' he he', begin
id                     └┘ └┘ └─┘
typ                    └┘ └┘ └─┘
st                                 └─────
438      replace he : e ∈ atlas H H := he,
id                      └───┘       └┘
src      └───────────┘ └───┘  └──┘
typ      └───────────┘└───┘ └──┘└┘
doc      └───────────┘         └──┘
txt      └───────────┘         └──┘
par      └───────────┘         └──┘
pid             └─┘└─┘         └──┘
st   ───────────────────────────────────┘└─
439      replace he' : e' ∈ atlas H H := he',
id                     └┘   └───┘       └─┘
src      └────────────┘   └───┘  └──┘
typ      └────────────┘└┘ └───┘ └──┘└─┘
doc      └────────────┘          └──┘
txt      └────────────┘          └──┘
par      └────────────┘          └──┘
pid             └──┘└─┘          └──┘
st   ──────────────────────────────────────┘└─
440      rw model_space_atlas at he he',
id          └───────────────┘
src      └─┘└───────────────┘└────────┘
typ      └─┘└───────────────┘└────────┘
doc      └─┘└───────────────┘└────────┘
txt      └─┘                 └────────┘
par      └─┘                 └────────┘
pid                         └────────┘
st   ─────────────────────────────────┘└─
441      simp [he, he', structure_groupoid.id_mem]
id             └┘  └─┘  └───────────────────────┘
src      └────┘  └┘   └┘└───────────────────────┘└─
typ      └────┘└┘└┘└─┘└┘└───────────────────────┘└─
doc      └────┘  └┘   └┘                         └─
txt      └────┘  └┘   └┘                         └─
par      └────┘  └┘   └┘                         └─
pid            └┘   └┘                         
st   ──────────────────────────────────────────────
442    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
443  
444  /-- Any manifold structure is compatible with the groupoid of all local homeomorphisms -/
445  instance has_groupoid_continuous_groupoid : has_groupoid M (continuous_groupoid H) :=
id                                               └──────────┘   └─────────────────┘ 
src                                              └──────────┘    └─────────────────┘
typ                                              └──────────┘   └─────────────────┘ 
doc                                              └──────────┘    └─────────────────┘
446  ⟨begin
st    └─────
447    assume e e' he he',
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid    └────────────────┘
st   ───────────────────┘└─
448    rw [continuous_groupoid, mem_groupoid_of_pregroupoid],
id         └─────────────────┘  └─────────────────────────┘
src    └──┘└─────────────────┘└┘└─────────────────────────┘
typ    └──┘└─────────────────┘└┘└─────────────────────────┘
doc    └──┘└─────────────────┘└┘                           
txt    └──┘                   └┘                           
par    └──┘                   └┘                           
pid      └┘                   └┘                           
st   ────────────────────────┘└───────────────────────────┘└──
449    simp only [and_self]
id                └──────┘
src    └─────────┘└──────┘└┘
typ    └─────────┘└──────┘└┘
doc    └─────────┘        └┘
txt    └─────────┘        └┘
par    └─────────┘        └┘
pid        └──┘└┘        
st   ──────────────────────┘
450  end⟩
st   └─┘
451  
452  /-- A G-diffeomorphism between two manifolds is a homeomorphism which, when read in the charts,
453  belongs to G. We avoid the word diffeomorph as it is too related to the smooth category, and use
454  structomorph instead. -/
455  structure structomorph (G : structure_groupoid H) (M : Type*) (M' : Type*)
id                               └────────────────┘        └───┘        └───┘
src                              └────────────────┘
typ                              └────────────────┘        └───┘        └───┘
doc                              └────────────────┘
456    [topological_space M] [topological_space M'] [manifold H M] [manifold H M']
id      └───────────────┘    └───────────────┘ └┘   └──────┘     └──────┘  └┘
src     └───────────────┘     └───────────────┘      └──────┘       └──────┘
typ     └───────────────┘    └───────────────┘ └┘   └──────┘     └──────┘  └┘
doc     └───────────────┘     └───────────────┘      └──────┘       └──────┘
457    extends homeomorph M M' :=
id             └────────┘  └┘
src            └────────┘
typ            └────────┘  └┘
doc            └────────┘
458  (to_fun_mem_groupoid : ∀c : local_homeomorph M H, ∀c' : local_homeomorph M' H,
id                              └──────────────┘          └──────────────┘ └┘ 
src                              └──────────────┘            └──────────────┘
typ                             └──────────────┘          └──────────────┘ └┘ 
doc                              └──────────────┘            └──────────────┘
459    c ∈ atlas H M → c' ∈ atlas H M' → c.symm ≫ₕ to_homeomorph.to_local_homeomorph ≫ₕ c' ∈ G)
id       └───┘     └┘  └───┘  └┘   └───┘ └┘ └───────────┘└──────────────────┘ └┘ └┘  
src       └───┘           └───┘         └───┘ └┘              └──────────────────┘ └┘    
typ      └───┘     └┘  └───┘  └┘   └───┘ └┘ └───────────┘└──────────────────┘ └┘ └┘  
doc                                       └───┘ └┘              └──────────────────┘ └┘
460  
461  variables [topological_space M'] [topological_space M'']
id              └───────────────┘      └───────────────┘
src             └───────────────┘      └───────────────┘
typ             └───────────────┘      └───────────────┘
doc             └───────────────┘      └───────────────┘
462  {G : structure_groupoid H} [manifold H M'] [manifold H M'']
id        └────────────────┘     └──────┘        └──────┘
src       └────────────────┘     └──────┘        └──────┘
typ       └────────────────┘     └──────┘        └──────┘
doc       └────────────────┘     └──────┘        └──────┘
463  
464  /-- The identity is a diffeomorphism of any manifold, for any groupoid. -/
465  def structomorph.refl (M : Type*) [topological_space M] [manifold H M]
id                                      └───────────────┘    └──────┘  
src                                     └───────────────┘     └──────┘
typ                                     └───────────────┘    └──────┘  
doc                                     └───────────────┘     └──────┘
466    [has_groupoid M G] : structomorph G M M :=
id      └──────────┘      └──────────┘   
src     └──────────┘        └──────────┘
typ     └──────────┘      └──────────┘   
doc     └──────────┘        └──────────┘
467  { to_fun_mem_groupoid := λc c' hc hc', begin
id                              └┘ └┘ └─┘
typ                             └┘ └┘ └─┘
st                                          └─────
468      change (local_homeomorph.symm c) ≫ₕ (local_homeomorph.refl M) ≫ₕ c' ∈ G,
id               └───────────────────┘   └┘  └───────────────────┘      └┘  
src      └─────┘ └───────────────────┘ └┘└┘ └───────────────────┘ └┘    
typ      └─────┘ └───────────────────┘└┘└┘ └───────────────────┘└┘  └┘
doc      └─────┘ └───────────────────┘ └┘└┘ └───────────────────┘ └┘     
txt      └─────┘                       └┘                         └┘     
par      └─────┘                       └┘                         └┘     
pid                                   └┘                         └┘     
st   ──────────────────────────────────────────────────────────────────────────┘└─
469      rw local_homeomorph.refl_trans,
id          └─────────────────────────┘
src      └─┘└─────────────────────────┘
typ      └─┘└─────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────────────────┘└─
470      exact has_groupoid.compatible G hc hc'
id             └─────────────────────┘  └┘ └─┘
src      └────┘└─────────────────────┘      
typ      └────┘└─────────────────────┘└┘└─┘
doc      └────┘                             
txt      └────┘                             
par      └────┘                             
pid                                        
st   ───────────────────────────────────────────
471    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
472    ..homeomorph.refl M }
id       └─────────────┘ 
src      └─────────────┘
typ      └─────────────┘ 
473  
474  /-- The inverse of a structomorphism is a structomorphism -/
475  def structomorph.symm (e : structomorph G M M') : structomorph G M' M :=
id                              └──────────┘   └┘    └──────────┘  └┘ 
src                             └──────────┘           └──────────┘
typ                             └──────────┘   └┘    └──────────┘  └┘ 
doc                             └──────────┘           └──────────┘
476  { to_fun_mem_groupoid := begin
st                            └─────
477      assume c c' hc hc',
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid      └────────────────┘
st   ─────────────────────┘└─
478      have : (c'.symm ≫ₕ e.to_homeomorph.to_local_homeomorph ≫ₕ c).symm ∈ G :=
id               └─────┘ └┘ └─────────────────────────────────┘            
src      └─────┘ └─────┘└┘└─────────────────────────────────┘   └─────┘ └───
typ      └─────┘ └─────┘└┘└─────────────────────────────────┘  └─────┘└───
doc      └─────┘ └─────┘└┘└─────────────────────────────────┘   └─────┘  └───
txt      └─────┘                                                └─────┘  └───
par      └─────┘                                                └─────┘  └───
pid      └───┘└┘                                                └─────┘  └───
st   ─────────────────────────────────────────────────────────────────────────────
479        G.inv _ (e.to_fun_mem_groupoid c' c hc' hc),
id         └───┘    └───────────────────┘ └┘  └─┘ └┘
src  ─────┘└───┘└─┘ └───────────────────┘        
typ  ─────┘└───┘└─┘ └───────────────────┘└┘└─┘└┘
doc  ─────┘     └─┘                              
txt  ─────┘     └─┘                              
par  ─────┘     └─┘                              
pid  ─────┘     └─┘                              
st   ────────────────────────────────────────────────┘└─
480      simp at this,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid          └─────┘
st   ───────────────┘└─
481      rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
id            └───────────────────────────┘  └───────────────────────────┘  └───────┘  └─────────┘
src      └───┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────┘└┘└─────────┘└─
typ      └───┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────┘└┘└─────────┘└─
doc      └───┘                             └┘                             └┘         └┘           └─
txt      └───┘                             └┘                             └┘         └┘           └─
par      └───┘                             └┘                             └┘         └┘           └─
pid         └┘                             └┘                             └┘         └┘           
st   ─────────────────────────────────────┘└─────────────────────────────┘└─────────┘└───────────┘
482        at this,
src  ────────────┘
typ  ────────────┘
doc  ────────────┘
txt  ────────────┘
par  ────────────┘
pid  ────────────┘
st   ────────────┘└─
483    end,
st   ────┘
484    ..e.to_homeomorph.symm}
id       └────────────┘└───┘
src       └────────────┘└───┘
typ      └────────────┘└───┘
485  
486  /-- The composition of structomorphisms is a structomorphism -/
487  def structomorph.trans (e : structomorph G M M') (e' : structomorph G M' M'') : structomorph G M M'' :=
id                               └──────────┘   └┘        └──────────┘  └┘ └─┘    └──────────┘   └─┘
src                              └──────────┘               └──────────┘             └──────────┘
typ                              └──────────┘   └┘        └──────────┘  └┘ └─┘    └──────────┘   └─┘
doc                              └──────────┘               └──────────┘             └──────────┘
488  { to_fun_mem_groupoid := begin
st                            └─────
489      /- Let c and c' be two charts in M and M''. We want to show that e' ∘ e is smooth in these
st   ───────────────────────────────────────────────────────────────────────────────────────────────
490      charts, around any point x. For this, let y = e (c⁻¹ x), and consider a chart g around y.
st   ──────────────────────────────────────────────────────────────────────────────────────────────
491      Then g ∘ e ∘ c⁻¹ and c' ∘ e' ∘ g⁻¹ are both smooth as e and e' are structomorphisms, so
st   ────────────────────────────────────────────────────────────────────────────────────────────
492      their composition is smooth, and it coincides with c' ∘ e' ∘ e ∘ c⁻¹ around x. -/
st   ──────────────────────────────────────────────────────────────────────────────────────
493      assume c c' hc hc',
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid      └────────────────┘
st   ─────────────────────┘└─
494      refine G.locality _ (λx hx, _),
id              └────────┘
src      └─────┘└────────┘└─┘  └──────┘
typ      └─────┘└────────┘└─┘  └──────┘
doc      └─────┘          └─┘  └──────┘
txt      └─────┘          └─┘  └──────┘
par      └─────┘          └─┘  └──────┘
pid                      └─┘  └──────┘
st   ─────────────────────────────────┘└─
495      let f₁ := e.to_homeomorph.to_local_homeomorph,
id                 └─────────────────────────────────┘
src      └────────┘└─────────────────────────────────┘
typ      └────────┘└─────────────────────────────────┘
doc      └────────┘└─────────────────────────────────┘
txt      └────────┘
par      └────────┘
pid      └────┘└─┘
st   ────────────────────────────────────────────────┘└─
496      let f₂ := e'.to_homeomorph.to_local_homeomorph,
id                 └──────────────────────────────────┘
src      └────────┘└──────────────────────────────────┘
typ      └────────┘└──────────────────────────────────┘
doc      └────────┘└──────────────────────────────────┘
txt      └────────┘
par      └────────┘
pid      └────┘└─┘
st   ─────────────────────────────────────────────────┘└─
497      let f  := (e.to_homeomorph.trans e'.to_homeomorph).to_local_homeomorph,
id                  └───────────────────┘ └──────────────┘
src      └────────┘ └───────────────────┘└──────────────┘└───────────────────┘
typ      └────────┘ └───────────────────┘└──────────────┘└───────────────────┘
doc      └────────┘                                      └───────────────────┘
txt      └────────┘                                      └───────────────────┘
par      └────────┘                                      └───────────────────┘
pid      └───┘└┘└─┘                                      └──────────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
498      have feq : f = f₁ ≫ₕ f₂ := homeomorph.trans_to_local_homeomorph _ _,
id                    └┘ └┘ └┘    └──────────────────────────────────┘
src      └─────────┘   └┘  └──┘└──────────────────────────────────┘└──┘
typ      └─────────┘└┘└┘└┘└──┘└──────────────────────────────────┘└──┘
doc      └─────────┘    └┘  └──┘                                    └──┘
txt      └─────────┘        └──┘                                    └──┘
par      └─────────┘        └──┘                                    └──┘
pid      └──────┘└─┘        └──┘                                    └──┘
st   ──────────────────────────────────────────────────────────────────────┘└─
499      -- define the atlas g around y
st   ───────────────────────────────────
500      let y := (c.symm ≫ₕ f₁).to_fun x,
id                 └────┘    └┘         
src      └───────┘ └────┘    └───────┘
typ      └───────┘ └────┘  └┘└───────┘
doc      └───────┘ └────┘    └───────┘
txt      └───────┘           └───────┘
par      └───────┘           └───────┘
pid      └───┘└─┘           └───────┘
st   ───────────────────────────────────┘└─
501      let g := chart_at H y,
id                └──────┘  
src      └───────┘└──────┘ 
typ      └───────┘└──────┘
doc      └───────┘         
txt      └───────┘         
par      └───────┘         
pid      └───┘└─┘         
st   ────────────────────────┘└─
502      have hg₁ := chart_mem_atlas H y,
id                   └─────────────┘  
src      └──────────┘└─────────────┘ 
typ      └──────────┘└─────────────┘
doc      └──────────┘                
txt      └──────────┘                
par      └──────────┘                
pid      └──────┘└─┘                
st   ──────────────────────────────────┘└─
503      have hg₂ := mem_chart_source H y,
id                   └──────────────┘  
src      └──────────┘└──────────────┘ 
typ      └──────────┘└──────────────┘
doc      └──────────┘                 
txt      └──────────┘                 
par      └──────────┘                 
pid      └──────┘└─┘                 
st   ───────────────────────────────────┘└─
504      let s := (c.symm ≫ₕ f₁).source ∩ (c.symm ≫ₕ f₁).to_fun ⁻¹' g.source,
id                                        └────┘    └┘         └─┘ └──────┘
src      └───────┘           └───────┘ └────┘    └───────┘└─┘└──────┘
typ      └───────┘           └───────┘ └────┘  └┘└───────┘└─┘└──────┘
doc      └───────┘           └───────┘  └────┘    └───────┘└─┘
txt      └───────┘           └───────┘            └───────┘   
par      └───────┘           └───────┘            └───────┘   
pid      └───┘└─┘           └───────┘            └───────┘   
st   ──────────────────────────────────────────────────────────────────────┘└─
505      have open_s : is_open s,
id                     └─────┘ 
src      └────────────┘└─────┘
typ      └────────────┘└─────┘
doc      └────────────┘└─────┘
txt      └────────────┘       
par      └────────────┘       
pid      └─────────┘└─┘       
st   ──────────────────────────┘
506        by apply (c.symm ≫ₕ f₁).continuous_to_fun.preimage_open_of_open; apply open_source,
id                   └────┘    └┘                                                 └─────────┘
src           └────┘ └────┘    └───────────────────────────────────────┘  └────┘└─────────┘
typ           └────┘ └────┘  └┘└───────────────────────────────────────┘  └────┘└─────────┘
doc           └────┘ └────┘    └───────────────────────────────────────┘  └────┘
txt           └────┘           └───────────────────────────────────────┘  └────┘
par           └────┘           └───────────────────────────────────────┘  └────┘
pid                           └──────────────────────────────────────┘       
st                                                                                           └─
507      have : x ∈ s,
id                
src      └─────┘ 
typ      └─────┘
doc      └─────┘  
txt      └─────┘  
par      └─────┘  
pid      └───┘└┘  
st   ───────────────┘└─
508      { split,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ─────┘└───┘└─
509        { simp only [trans_source, preimage_univ, inter_univ, homeomorph.to_local_homeomorph_source],
id                      └──────────┘  └───────────┘  └────────┘  └───────────────────────────────────┘
src          └─────────┘└──────────┘└┘└───────────┘└┘└────────┘└┘└───────────────────────────────────┘
typ          └─────────┘└──────────┘└┘└───────────┘└┘└────────┘└┘└───────────────────────────────────┘
doc          └─────────┘            └┘             └┘          └┘                                     
txt          └─────────┘            └┘             └┘          └┘                                     
par          └─────────┘            └┘             └┘          └┘                                     
pid              └──┘└┘            └┘             └┘          └┘                                     
st   ───────┘└────────────────────────────────────────────────────────────────────────────────────────┘└─
510          rw trans_source at hx,
id              └──────────┘
src          └─┘└──────────┘└────┘
typ          └─┘└──────────┘└────┘
doc          └─┘            └────┘
txt          └─┘            └────┘
par          └─┘            └────┘
pid                        └────┘
st   ────────────────────────────┘└─
511          exact hx.1 },
id                 └┘
src          └────┘  └─┘
typ          └────┘└┘└─┘
doc          └────┘  └─┘
txt          └────┘  └─┘
par          └────┘  └─┘
pid                 └─┘
st   ──────────────────┘└┘
512        { exact hg₂ } },
id                 └─┘
src          └────┘   
typ          └────┘└─┘
doc          └────┘   
txt          └────┘   
par          └────┘   
pid                  
st   ─────────────────┘└──┘
513      refine ⟨s, open_s, ⟨this, _⟩⟩,
id                 └────┘   └──┘
src      └─────┘  └┘      └┘     └───┘
typ      └─────┘ └┘└────┘└┘ └──┘└───┘
doc      └─────┘  └┘      └┘     └───┘
txt      └─────┘  └┘      └┘     └───┘
par      └─────┘  └┘      └┘     └───┘
pid              └┘      └┘     └───┘
st   ────────────────────────────────┘└─
514      let F₁ := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ (g.symm ≫ₕ f₂ ≫ₕ c'),
id                  └────┘    └┘           └────┘    └┘    └┘
src      └────────┘ └────┘       └┘   └────┘        
typ      └────────┘ └────┘  └┘   └┘   └────┘  └┘  └┘
doc      └────────┘ └────┘       └┘   └────┘        
txt      └────────┘              └┘                 
par      └────────┘              └┘                 
pid      └────┘└─┘              └┘                 
st   ────────────────────────────────────────────────────────┘└─
515      have A : F₁ ∈ G :=
id                └┘   
src      └───────┘    └───
typ      └───────┘└┘ └───
doc      └───────┘    └───
txt      └───────┘    └───
par      └───────┘    └───
pid      └────┘└─┘    └───
st   ───────────────────────
516        G.comp _ _ (e.to_fun_mem_groupoid c g hc hg₁) (e'.to_fun_mem_groupoid g c' hg₁ hc'),
id         └────┘      └───────────────────┘    └┘       └────────────────────┘  └┘ └─┘ └─┘
src  ─────┘└────┘└───┘ └───────────────────┘       └┘ └────────────────────┘         
typ  ─────┘└────┘└───┘ └───────────────────┘ └┘   └┘ └────────────────────┘└┘└─┘└─┘
doc  ─────┘      └───┘                             └┘                                
txt  ─────┘      └───┘                             └┘                                
par  ─────┘      └───┘                             └┘                                
pid  ─────┘      └───┘                             └┘                                
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
517      let F₂ := (c.symm ≫ₕ f ≫ₕ c').restr s,
id                  └────┘        └┘        
src      └────────┘ └────┘       └──────┘
typ      └────────┘ └────┘    └┘└──────┘
doc      └────────┘ └────┘       └──────┘
txt      └────────┘              └──────┘
par      └────────┘              └──────┘
pid      └────┘└─┘              └──────┘
st   ────────────────────────────────────────┘└─
518      have : F₁ ≈ F₂ := calc
id              └┘  └┘
src      └─────┘    └──┘    
typ      └─────┘└┘└┘└──┘    
doc      └─────┘     └──┘    
txt      └─────┘     └──┘    
par      └─────┘     └──┘    
pid      └───┘└┘     └──┘    
st   ───────────────────────────
519        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' : by simp [F₁, trans_assoc]
id         └┘   └────┘    └┘          └────┘     └┘    └┘            └┘  └─────────┘
src  ─────┘   └────┘          └────┘└┘        └─┘  └────┘  └┘└─────────┘└─
typ  ─────┘└┘ └────┘  └┘      └────┘└┘  └┘  └┘└─┘  └────┘└┘└┘└─────────┘└─
doc  ─────┘   └────┘          └────┘└┘        └─┘  └────┘  └┘           └─
txt  ─────┘                         └┘        └─┘  └────┘  └┘           └─
par  ─────┘                         └┘        └─┘  └────┘  └┘           └─
pid  ─────┘                         └┘        └─┘  └─────┘  └┘           └─
st   ────────────────────────────────────────────────────────┘└───────────────────────
520        ... ≈ c.symm ≫ₕ f₁ ≫ₕ (of_set g.source g.open_source) ≫ₕ f₂ ≫ₕ c' :
id                                └────┘ └──────┘ └───────────┘
src  ─────┘└──┘              └────┘└──────┘└───────────┘└┘        └──
typ  ─────┘└──┘              └────┘└──────┘└───────────┘└┘        └──
doc  ─────┘└──┘              └────┘                     └┘        └──
txt  ─────┘└──┘                                         └┘        └──
par  ─────┘└──┘                                         └┘        └──
pid  ─────────┘                                         └┘        └──
st   ─────┘└───────────────────────────────────────────────────────────────────
521          by simp [eq_on_source_trans, trans_self_symm g]
id                    └────────────────┘  └─────────────┘ 
src  ───────┘  └────┘└────────────────┘└┘└─────────────┘ └─
typ  ───────┘  └────┘└────────────────┘└┘└─────────────┘└─
doc  ───────┘  └────┘└────────────────┘└┘└─────────────┘ └─
txt  ───────┘  └────┘                  └┘                └─
par  ───────┘  └────┘                  └┘                └─
pid  ───────┘  └─────┘                  └┘                └─
st   ─────────┘└─────────────────────────────────────────────
522        ... ≈ ((c.symm ≫ₕ f₁) ≫ₕ (of_set g.source g.open_source)) ≫ₕ (f₂ ≫ₕ c') :
src  ─────┘└──┘             └┘                              └─┘         └───
typ  ─────┘└──┘             └┘                              └─┘         └───
doc  ─────┘└──┘             └┘                              └─┘         └───
txt  ─────┘└──┘             └┘                              └─┘         └───
par  ─────┘└──┘             └┘                              └─┘         └───
pid  ─────────┘             └┘                              └─┘         └───
st   ─────┘└─────────────────────────────────────────────────────────────────────────
523          by simp [trans_assoc]
id                    └─────────┘
src  ───────┘  └────┘└─────────┘└─
typ  ───────┘  └────┘└─────────┘└─
doc  ───────┘  └────┘           └─
txt  ───────┘  └────┘           └─
par  ───────┘  └────┘           └─
pid  ───────┘  └─────┘           └─
st   ─────────┘└───────────────────
524        ... ≈ ((c.symm ≫ₕ f₁).restr s) ≫ₕ (f₂ ≫ₕ c') : by simp [s, trans_of_set']
id                                                                  └───────────┘
src  ─────┘└──┘             └──────┘ └┘         └──┘  └────┘ └┘└───────────┘└─
typ  ─────┘└──┘             └──────┘└┘         └──┘  └────┘└┘└───────────┘└─
doc  ─────┘└──┘             └──────┘ └┘         └──┘  └────┘ └┘             └─
txt  ─────┘└──┘             └──────┘ └┘         └──┘  └────┘ └┘             └─
par  ─────┘└──┘             └──────┘ └┘         └──┘  └────┘ └┘             └─
pid  ─────────┘             └──────┘ └┘         └──┘  └─────┘ └┘             └─
st   ─────┘└───────────────────────────────────────────────┘└────────────────────────
525        ... ≈ ((c.symm ≫ₕ f₁) ≫ₕ (f₂ ≫ₕ c')).restr s : by simp [restr_trans]
id                                                                 └─────────┘
src  ─────┘└──┘             └┘         └───────┘ └─┘  └────┘└─────────┘└─
typ  ─────┘└──┘             └┘         └───────┘ └─┘  └────┘└─────────┘└─
doc  ─────┘└──┘             └┘         └───────┘ └─┘  └────┘           └─
txt  ─────┘└──┘             └┘         └───────┘ └─┘  └────┘           └─
par  ─────┘└──┘             └┘         └───────┘ └─┘  └────┘           └─
pid  ─────────┘             └┘         └───────┘ └─┘  └─────┘           └─
st   ─────┘└───────────────────────────────────────────────┘└───────────────────
526        ... ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s : by simp [eq_on_source_restr, trans_assoc]
id                                                               └────────────────┘  └─────────┘
src  ─────┘└──┘                 └┘    └──────┘ └─┘  └────┘└────────────────┘└┘└─────────┘└─
typ  ─────┘└──┘                 └┘    └──────┘ └─┘  └────┘└────────────────┘└┘└─────────┘└─
doc  ─────┘└──┘                 └┘    └──────┘ └─┘  └────┘└────────────────┘└┘           └─
txt  ─────┘└──┘                 └┘    └──────┘ └─┘  └────┘                  └┘           └─
par  ─────┘└──┘                 └┘    └──────┘ └─┘  └────┘                  └┘           └─
pid  ─────────┘                 └┘    └──────┘ └─┘  └─────┘                  └┘           └─
st   ─────┘└─────────────────────────────────────────────┘└───────────────────────────────────────
527        ... ≈ F₂ : by simp [F₂, feq],
id               └┘            └┘  └─┘
src  ─────┘└──┘   └─┘  └────┘  └┘   
typ  ─────┘└──┘ └┘└─┘  └────┘└┘└┘└─┘
doc  ─────┘└──┘   └─┘  └────┘  └┘   
txt  ─────┘└──┘   └─┘  └────┘  └┘   
par  ─────┘└──┘   └─┘  └────┘  └┘   
pid  ─────────┘   └─┘  └─────┘  └┘   
st   ─────┘└───────────┘└─────────────┘└─
528      have : F₂ ∈ G := G.eq_on_source F₁ F₂ A (setoid.symm this),
id              └┘       └────────────┘ └┘ └┘   └─────────┘ └──┘
src      └─────┘    └──┘└────────────┘      └─────────┘    
typ      └─────┘└┘ └──┘└────────────┘└┘└┘ └─────────┘└──┘
doc      └─────┘    └──┘                                   
txt      └─────┘    └──┘                                   
par      └─────┘    └──┘                                   
pid      └───┘└┘    └──┘                                   
st   ─────────────────────────────────────────────────────────────┘└─
529      exact this
id             └──┘
src      └────┘    
typ      └────┘└──┘
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───────────────
530    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
531    ..homeomorph.trans e.to_homeomorph e'.to_homeomorph }
id       └──────────────┘ └────────────┘ └┘└────────────┘
src      └──────────────┘  └────────────┘   └────────────┘
typ      └──────────────┘ └────────────┘ └┘└────────────┘
532  
533  end has_groupoid